To formally construct, i.e. to prove the existence of a certain function of one variable, you start with two, not necessarily distinct, sets: a domain set (x) and a codomain set (y). Then construct the Cartesian product of the domain and codomain sets (xy). (See sample proof below.)

Using the Subset Axiom, we then construct the graph set (g) of the function in question as a subset of x*y.

If, for all a in x, there exists a unique b in y such that (a, b) in g, then, using the Function Axiom, you can infer the existence of a function f such that:

ALL(a): ALL(b): [a in x & b in y => [ f(a)=b <=> (a, b) in g]

Then it is easy to prove:

ALL(a): [a in x => f(a) in y]

ALL(a): [a in x => (a, f(a)) in g]

In DC Proof, we have the following sample proof:

Let x and y be sets

1. Set(x)
Axiom

2. Set(y)
Axiom

Apply the Cartesian Product Axiom

3. ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) in b <=> c1 in a1 & c2 in a2]]]
Cart Prod

4. ALL(a2):[Set(x) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) in b <=> c1 in x & c2 in a2]]]
U Spec, 3

5. Set(x) & Set(y) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) in b <=> c1 in x & c2 in y]]
U Spec, 4

6. Set(x) & Set(y)
Join, 1, 2

7. EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) in b <=> c1 in x & c2 in y]]
Detach, 5, 6

Define: xy (The Cartesian product of sets x and y)

8. Set'(xy) & ALL(c1):ALL(c2):[(c1,c2) in xy <=> c1 in x & c2 in y]
E Spec, 7

9. Set'(xy)
Split, 8

10. ALL(c1):ALL(c2):[(c1,c2) in xy <=> c1 in x & c2 in y]
Split, 8

Apply the Subset Axiom where P is the selection criteria

11. EXIST(a):[Set'(a) & ALL(b):ALL(c):[(b,c) in a <=> (b,c) in xy & P(b,c)]]
Subset, 9

Define: g (the graph set)

12. Set'(g) & ALL(b):ALL(c):[(b,c) in g <=> (b,c) in xy & P(b,c)]
E Spec, 11

13. Set'(g)
Split, 12

14. ALL(b):ALL(c):[(b,c) in g <=> (b,c) in xy & P(b,c)]
Split, 12

Apply the Function Axiom (for 1 variable)

15. ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
=> [ALL(a1):ALL(b):[(a1,b) in gra => a1 in dom & b in cod]
& ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 in dom & b1 in cod & b2 in cod
=> [(a1,b1) in gra & (a1,b2) in gra => b1=b2]]
=> EXIST(fun):ALL(a1):ALL(b):[a1 in dom & b in cod
=> [fun(a1)=b <=> (a1,b) in gra]]]]
Function

Substituting x, y, g for dom, cod and graph respectively...

16. ALL(cod):ALL(gra):[Set(x) & Set(cod) & Set'(gra)
=> [ALL(a1):ALL(b):[(a1,b) in gra => a1 in x & b in cod]
& ALL(a1):[a1 in x => EXIST(b):[b in cod & (a1,b) in gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 in x & b1 in cod & b2 in cod
=> [(a1,b1) in gra & (a1,b2) in gra => b1=b2]]
=> EXIST(fun):ALL(a1):ALL(b):[a1 in x & b in cod
=> [fun(a1)=b <=> (a1,b) in gra]]]]
U Spec, 15

17. ALL(gra):[Set(x) & Set(y) & Set'(gra)
=> [ALL(a1):ALL(b):[(a1,b) in gra => a1 in x & b in y]
& ALL(a1):[a1 in x => EXIST(b):[b in y & (a1,b) in gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 in x & b1 in y & b2 in y
=> [(a1,b1) in gra & (a1,b2) in gra => b1=b2]]
=> EXIST(fun):ALL(a1):ALL(b):[a1 in x & b in y
=> [fun(a1)=b <=> (a1,b) in gra]]]]
U Spec, 16

18. Set(x) & Set(y) & Set'(g)
=> [ALL(a1):ALL(b):[(a1,b) in g => a1 in x & b in y]
& ALL(a1):[a1 in x => EXIST(b):[b in y & (a1,b) in g]]
& ALL(a1):ALL(b1):ALL(b2):[a1 in x & b1 in y & b2 in y
=> [(a1,b1) in g & (a1,b2) in g => b1=b2]]
=> EXIST(fun):ALL(a1):ALL(b):[a1 in x & b in y
=> [fun(a1)=b <=> (a1,b) in g]]]
U Spec, 17

19. Set(x) & Set(y) & Set'(g)
Join, 6, 13

Sufficient: For functionality based on graph set g

20. ALL(a1):ALL(b):[(a1,b) in g => a1 in x & b in y]
& ALL(a1):[a1 in x => EXIST(b):[b in y & (a1,b) in g]]
& ALL(a1):ALL(b1):ALL(b2):[a1 in x & b1 in y & b2 in y
=> [(a1,b1) in g & (a1,b2) in g => b1=b2]]

=> EXIST(fun):ALL(a1):ALL(b):[a1 in x & b in y => [fun(a1)=b <=> (a1,b) in g]]
Detach, 18, 19

<end of sample>

Some may be tempted to obtain simply: ALL(a):ALL(b):[fun(a)=b <=> (a,b) in g]

But this may lead us into Burse's Paradox where inferences are obtained about a function outside of its domain of definition--truly something to be avoided in mathematics.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

On Saturday, February 19, 2022 at 4:22:45 PM UTC-5, Dan Christensen wrote:
> To formally construct, i.e. to prove the existence of a certain function of one variable, you start with two, not necessarily distinct, sets: a domain set (x) and a codomain set (y). Then construct the Cartesian product of the domain and codomain sets (xy). (See sample proof below.)
>
> Using the Subset Axiom, we then construct the graph set (g) of the function in question as a subset of x*y.
>
> If, for all a in x, there exists a unique b in y such that (a, b) in g, then, using the Function Axiom, you can infer the existence of a function f such that:
>
> ALL(a): ALL(b): [a in x & b in y => [ f(a)=b <=> (a, b) in g]
>
> Then it is easy to prove:
>
> ALL(a): [a in x => f(a) in y]
>
> ALL(a): [a in x => (a, f(a)) in g]
>
> In DC Proof, we have the following sample proof:
>
> Let x and y be sets
>
> 1. Set(x)
> Axiom
>
> 2. Set(y)
> Axiom
>
> Apply the Cartesian Product Axiom
>
> 3. ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) in b <=> c1 in a1 & c2 in a2]]]
> Cart Prod
>
> 4. ALL(a2):[Set(x) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) in b <=> c1 in x & c2 in a2]]]
> U Spec, 3
>
> 5. Set(x) & Set(y) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) in b <=> c1 in x & c2 in y]]
> U Spec, 4
>
> 6. Set(x) & Set(y)
> Join, 1, 2
>
> 7. EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) in b <=> c1 in x & c2 in y]]
> Detach, 5, 6
>
> Define: xy (The Cartesian product of sets x and y)
>
> 8. Set'(xy) & ALL(c1):ALL(c2):[(c1,c2) in xy <=> c1 in x & c2 in y]
> E Spec, 7
>
> 9. Set'(xy)
> Split, 8
>
> 10. ALL(c1):ALL(c2):[(c1,c2) in xy <=> c1 in x & c2 in y]
> Split, 8
>
> Apply the Subset Axiom where P is the selection criteria
>
> 11. EXIST(a):[Set'(a) & ALL(b):ALL(c):[(b,c) in a <=> (b,c) in xy & P(b,c)]]
> Subset, 9
>
> Define: g (the graph set)
>
> 12. Set'(g) & ALL(b):ALL(c):[(b,c) in g <=> (b,c) in xy & P(b,c)]
> E Spec, 11
>
> 13. Set'(g)
> Split, 12
>
> 14. ALL(b):ALL(c):[(b,c) in g <=> (b,c) in xy & P(b,c)]
> Split, 12
>
> Apply the Function Axiom (for 1 variable)
>
> 15. ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
> => [ALL(a1):ALL(b):[(a1,b) in gra => a1 in dom & b in cod]
> & ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in gra]]
> & ALL(a1):ALL(b1):ALL(b2):[a1 in dom & b1 in cod & b2 in cod
> => [(a1,b1) in gra & (a1,b2) in gra => b1=b2]]
> => EXIST(fun):ALL(a1):ALL(b):[a1 in dom & b in cod
> => [fun(a1)=b <=> (a1,b) in gra]]]]
> Function
>
> Substituting x, y, g for dom, cod and graph respectively...
>
> 16. ALL(cod):ALL(gra):[Set(x) & Set(cod) & Set'(gra)
> => [ALL(a1):ALL(b):[(a1,b) in gra => a1 in x & b in cod]
> & ALL(a1):[a1 in x => EXIST(b):[b in cod & (a1,b) in gra]]
> & ALL(a1):ALL(b1):ALL(b2):[a1 in x & b1 in cod & b2 in cod
> => [(a1,b1) in gra & (a1,b2) in gra => b1=b2]]
> => EXIST(fun):ALL(a1):ALL(b):[a1 in x & b in cod
> => [fun(a1)=b <=> (a1,b) in gra]]]]
> U Spec, 15
>
> 17. ALL(gra):[Set(x) & Set(y) & Set'(gra)
> => [ALL(a1):ALL(b):[(a1,b) in gra => a1 in x & b in y]
> & ALL(a1):[a1 in x => EXIST(b):[b in y & (a1,b) in gra]]
> & ALL(a1):ALL(b1):ALL(b2):[a1 in x & b1 in y & b2 in y
> => [(a1,b1) in gra & (a1,b2) in gra => b1=b2]]
> => EXIST(fun):ALL(a1):ALL(b):[a1 in x & b in y
> => [fun(a1)=b <=> (a1,b) in gra]]]]
> U Spec, 16
>
> 18. Set(x) & Set(y) & Set'(g)
> => [ALL(a1):ALL(b):[(a1,b) in g => a1 in x & b in y]
> & ALL(a1):[a1 in x => EXIST(b):[b in y & (a1,b) in g]]
> & ALL(a1):ALL(b1):ALL(b2):[a1 in x & b1 in y & b2 in y
> => [(a1,b1) in g & (a1,b2) in g => b1=b2]]
> => EXIST(fun):ALL(a1):ALL(b):[a1 in x & b in y
> => [fun(a1)=b <=> (a1,b) in g]]]
> U Spec, 17
>
> 19. Set(x) & Set(y) & Set'(g)
> Join, 6, 13
>
> Sufficient: For functionality based on graph set g
>
> 20. ALL(a1):ALL(b):[(a1,b) in g => a1 in x & b in y]
> & ALL(a1):[a1 in x => EXIST(b):[b in y & (a1,b) in g]]
> & ALL(a1):ALL(b1):ALL(b2):[a1 in x & b1 in y & b2 in y
> => [(a1,b1) in g & (a1,b2) in g => b1=b2]]
>
> => EXIST(fun):ALL(a1):ALL(b):[a1 in x & b in y => [fun(a1)=b <=> (a1,b) in g]]
> Detach, 18, 19
>
> <end of sample>
>
> Some may be tempted to obtain simply: ALL(a):ALL(b):[fun(a)=b <=> (a,b) in g]
>

Without restrictions on the quantifiers as here, we may obtain bizarre inferences (Burse's Paradox) about functions outside of their domain of definition--truly something to be avoided in mathematics.

>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Dan Christensen wrote:

> If, for all a in x, there exists a unique b in y such that (a, b) in g,
> then, using the Function Axiom, you can infer the existence of a
> function f such that:
> ALL(a): ALL(b): [a in x & b in y => [ f(a)=b <=> (a, b) in g]

the filthy LGBTQ+ capitalist west is arming already ukraine, as they did
arme Hitler 1939. The german "war_machine" was *pure* west business, not
gearmon. Many reasons.

then now Ukraine launches US nukes into Russia, to preemptively destroy
Russia's capability to "attack" Ukraine someday in the future. NATO okays
this first strike, as it is a purely defensive move. Russia lies in ruins,
hundreds of millions dead. This fate awaits Russia should they do NOTHING
to stop NATO now.

Ukraine threatens to renounce its non-nuclear status
https://www.rt.com/russia/549994-ukraine-threatens-renounce-memorandum/

Apparently Swedish defense is having some drills with the American
military escorting an American bombplane B-52 Stratofortress flying over
south of Sweden. At the end of the article the formulation is weird as
here the reporter comments about having nuclear arms in Sweden. So the
drills had a mission of transporting nuclear arms to Sweden

On Saturday, February 19, 2022 at 5:14:24 PM UTC-5, Bradlee Evers wrote:
> Dan Christensen wrote:
>
> > If, for all a in x, there exists a unique b in y such that (a, b) in g,
> > then, using the Function Axiom, you can infer the existence of a
> > function f such that:
> > ALL(a): ALL(b): [a in x & b in y => [ f(a)=b <=> (a, b) in g]
> the filthy LGBTQ+ capitalist west is arming already ukraine, as they did
> arme Hitler 1939. The german "war_machine" was *pure* west business, not
> gearmon. Many reasons.
>

So Comrade Putin has directed you to switch your attention from attacking COVID measures in the West to attacking Ukraine. Interesting. But your disinformation on COVID has somewhat undermined your new efforts.

Dan Christensen wrote:

>> > ALL(a): ALL(b): [a in x & b in y => [ f(a)=b <=> (a, b) in g]
>> the filthy LGBTQ+ capitalist west is arming already ukraine, as they
>> did arme Hitler 1939. The german "war_machine" was *pure* west
>> business, not gearmon. Many reasons.
>
> So Comrade Putin has directed you to switch your attention from
> attacking COVID measures in the West to attacking Ukraine.

"covid measures"?? you stupid uneducated bitch. Turns out from the
beginning it was just a code boiled on a computer. You disgusting lying
bitch. One day he says war, next day he says peace, the third day he says
he would get nuclear weapons. Wise puppet.

On 2/19/2022 5:37 PM, Dan Christensen wrote:
> On Saturday, February 19, 2022 at 5:14:24 PM UTC-5, Bradlee Evers wrote:
>> Dan Christensen wrote:
>>
>>> If, for all a in x, there exists a unique b in y such that (a, b) in g,
>>> then, using the Function Axiom, you can infer the existence of a
>>> function f such that:
>>> ALL(a): ALL(b): [a in x & b in y => [ f(a)=b <=> (a, b) in g]
>> the filthy LGBTQ+ capitalist west is arming already ukraine, as they did
>> arme Hitler 1939. The german "war_machine" was *pure* west business, not
>> gearmon. Many reasons.
>>
>
> So Comrade Putin has directed you to switch your attention from attacking COVID measures in the West to attacking Ukraine. Interesting. But your disinformation on COVID has somewhat undermined your new efforts.

Poor nymshifter. Ever since its beloved Yugoslavia disintegrated, it
wound up in just about the poorest country in Europe, and now it has to
take orders from its Soviet, err, I mean, Russian slavemasters to spread
their disinformation.

(Dan, you may remember, it was spreading disinformation on the US
presidential election before Covid hit)

Michael Moroney wrote:

>> So Comrade Putin has directed you to switch your attention from
>> attacking COVID measures in the West to attacking Ukraine.
>> Interesting.
>> But your disinformation on COVID has somewhat undermined your new
>> efforts.
>
> Poor nymshifter. Ever since its beloved Yugoslavia disintegrated, it
> wound up in just about the poorest country in Europe, and now it has to
> take orders from its Soviet, err, I mean, Russian slavemasters to spread
> their disinformation.
>
> (Dan, you may remember, it was spreading disinformation on the US
> presidential election before Covid hit)

you made ukraine the *poorest_nazi_hole* in europe, you stinking shit. And
what "US presidential election", you fucking imbecile, lol.

These repulsive trolls, wants people dead with mortal injections, truly
believe in "presidential elections", which emphasise the imbeciles they
are. You two *mass_murderers* will hang in trees, now that the cacanada
and austreilia are forced in deep shit by their own people. You repugnant
sack of shit, "US presidential elections". lol.

On Saturday, February 19, 2022 at 10:24:50 PM UTC-5, Bradlee Evers wrote:
> Michael Moroney wrote:
>
> >> So Comrade Putin has directed you to switch your attention from
> >> attacking COVID measures in the West to attacking Ukraine.
> >> Interesting.
> >> But your disinformation on COVID has somewhat undermined your new
> >> efforts.
> >
> > Poor nymshifter. Ever since its beloved Yugoslavia disintegrated, it
> > wound up in just about the poorest country in Europe, and now it has to
> > take orders from its Soviet, err, I mean, Russian slavemasters to spread
> > their disinformation.
> >
> > (Dan, you may remember, it was spreading disinformation on the US
> > presidential election before Covid hit)
> you made ukraine the *poorest_nazi_hole* in europe, you stinking shit. And
> what "US presidential election", you fucking imbecile, lol.
>
> These repulsive trolls, wants people dead with mortal injections, truly
> believe in "presidential elections", which emphasise the imbeciles they
> are. You two *mass_murderers* will hang in trees, now that the cacanada
> and austreilia are forced in deep shit by their own people. You repugnant
> sack of shit, "US presidential elections". lol.

In terms of mg of venom per ruble, Putin is certainly getting his money's worth from you, Comrade X. You should ask him for a raise, enough to maybe get your own apartment.

Dan Christensen wrote:

>> These repulsive trolls, wants people dead with mortal injections, truly
>> believe in "presidential elections", which emphasise the imbeciles they
>> are. You two *mass_murderers* will hang in trees, now that the cacanada
>> and austreilia are forced in deep shit by their own people. You
>> repugnant sack of shit, "US presidential elections". lol.
>
> In terms of mg of venom per ruble, Putin is certainly getting his
> money's worth from you, Comrade X. You should ask him for a raise,
> enough to maybe get your own apartment.

Lots of land, he can chose anywhere, even in your fake money shithole
country, getting it for free. Then you get the sanctions, just to sense
how it feel like, with sanction.

But inbreed uneducated morons like you, promoting mortal injections to
kill people, never know the most and tallest skyscrapers in europe are
infact Russian. Pure art, beside the skyscrapers. Here we go, stupid.

Moscow Russia Aerial Drone 5K Timelab.pro _ Москва Россия Аэросъемка
https://www.youtube.com/watch?v=S_dfq9rFWAE