The equality of functions is usually defined as follows:

"Two functions f and g are equal if their domain and codomain sets are the same and their output values agree on the whole domain. More formally, given f: X → Y and g: X → Y, we have f = g if and only if f(x) = g(x) for all x ∈ X."
https://en.wikipedia.org/wiki/Function_(mathematics)#Definition

In the notation of DC Proof:

ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod)
& ALL(a):[a in dom => f(a) in cod]
& ALL(a):[a in dom => g(a) in cod]
=> [f=g <=> ALL(a):[a in dom => f(a)=g(a)]]]

Note that functions are comparable here only if they have the SAME domain and codomain.

Empty functions are defined as follows:

"For every set X, there is a unique function, called the empty function from the empty set to X."
https://en.wikipedia.org/wiki/Function_(mathematics)#Standard_functions

Here, I formally prove the uniqueness of such functions: https://dcproof.com/EqualityOfFunctions.htm (25 lines)

Dan

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

There is an error, you didn't lookup the wikipedia
definition of f: X → Y and you wrongly translate it to:

ALL(a):[a in dom => f(a) in cod]

Please lookup everything, not only the first thing
and then start halucinating your nonsense.

Dan Christensen schrieb am Montag, 28. März 2022 um 00:07:14 UTC+2:
> The equality of functions is usually defined as follows:
>
> "Two functions f and g are equal if their domain and codomain sets are the same and their output values agree on the whole domain. More formally, given f: X → Y and g: X → Y, we have f = g if and only if f(x) = g(x) for all x ∈ X."
> https://en.wikipedia.org/wiki/Function_(mathematics)#Definition
>
> In the notation of DC Proof:
>
> ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod)
> & ALL(a):[a in dom => f(a) in cod]
> & ALL(a):[a in dom => g(a) in cod]
> => [f=g <=> ALL(a):[a in dom => f(a)=g(a)]]]
>
> Note that functions are comparable here only if they have the SAME domain and codomain.
>
> Empty functions are defined as follows:
>
> "For every set X, there is a unique function, called the empty function from the empty set to X."
> https://en.wikipedia.org/wiki/Function_(mathematics)#Standard_functions
>
> Here, I formally prove the uniqueness of such functions: https://dcproof.com/EqualityOfFunctions.htm (25 lines)
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Sunday, March 27, 2022 at 7:08:12 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 28. März 2022 um 00:07:14 UTC+2:
> > The equality of functions is usually defined as follows:
> >
> > "Two functions f and g are equal if their domain and codomain sets are the same and their output values agree on the whole domain. More formally, given f: X → Y and g: X → Y, we have f = g if and only if f(x) = g(x) for all x ∈ X."
> > https://en.wikipedia.org/wiki/Function_(mathematics)#Definition
> >
> > In the notation of DC Proof:
> >
> > ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod)
> > & ALL(a):[a in dom => f(a) in cod]
> > & ALL(a):[a in dom => g(a) in cod]
> > => [f=g <=> ALL(a):[a in dom => f(a)=g(a)]]]
> >
> > Note that functions are comparable here only if they have the SAME domain and codomain.
> >
> > Empty functions are defined as follows:
> >
> > "For every set X, there is a unique function, called the empty function from the empty set to X."
> > https://en.wikipedia.org/wiki/Function_(mathematics)#Standard_functions
> >
> > Here, I formally prove the uniqueness of such functions: https://dcproof.com/EqualityOfFunctions.htm (25 lines)
> >

> There is an error, you didn't lookup the wikipedia
> definition of f: X → Y and you wrongly translate it to:
> ALL(a):[a in dom => f(a) in cod]

It's all fairly standard, Jan Burse. Face it, no one wants your "dark elements."

Dan

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