let X be set ; :: thesis: ( ( for f, g being Function st dom f = X & dom g = X holds
f = g ) implies X = {} )
deffunc H₁( object ) -> set = {} ;
assume A1: for f, g being Function st dom f = X & dom g = X holds
f = g ; :: thesis: X = {}
set x = the Element of X;
consider f being Function such that
A2: dom f = X and
A3: for x being object st x in X holds
f . x = H₁(x) from FUNCT_1:sch 3();
assume A4: not X = {} ; :: thesis: contradiction
then A5: f . the Element of X = {} by A3;
deffunc H₂( object ) -> set = {{}};
consider g being Function such that
A6: dom g = X and
A7: for x being object st x in X holds
g . x = H₂(x) from FUNCT_1:sch 3();
g . the Element of X = {{}} by A4, A7;
hence contradiction by A1, A2, A6, A5; :: thesis: verum