let X be set ; :: thesis: for x being object holds
( X, Funcs ({x},X) are_equipotent & card X = card (Funcs ({x},X)) )
let x be object ; :: thesis: ( X, Funcs ({x},X) are_equipotent & card X = card (Funcs ({x},X)) )
deffunc H1( object ) -> Element of bool [:{x},{$1}:] = {x} --> $1;
consider f being Function such that
A1: ( dom f = X & ( for y being object st y in X holds
f . y = H1(y) ) ) from FUNCT_1:sch 3();
 A2: x in {x} by TARSKI:def 1;
thus X, Funcs ({x},X) are_equipotent :: thesis: card X = card (Funcs ({x},X))
proof
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = X & proj2 f = Funcs ({x},X) )
thus f is one-to-one :: thesis: ( proj1 f = X & proj2 f = Funcs ({x},X) )
proof
let y, z be object ; :: according to FUNCT_1:def 4 :: thesis: ( not y in proj1 f or not z in proj1 f or not f . y = f . z or y = z )
assume ( y in dom f & z in dom f ) ; :: thesis: ( not f . y = f . z or y = z )
then A3: ( f . y = {x} --> y & f . z = {x} --> z ) by A1;
({x} --> y) . x = y by A2, FUNCOP_1:7;
hence ( not f . y = f . z or y = z ) by A2, A3, FUNCOP_1:7; :: thesis: verum
end;
thus dom f = X by A1; :: thesis: proj2 f = Funcs ({x},X)
thus rng f c= Funcs ({x},X) :: according to XBOOLE_0:def 10 :: thesis: Funcs ({x},X) c= proj2 f
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in Funcs ({x},X) )
assume y in rng f ; :: thesis: y in Funcs ({x},X)
then consider z being object such that
A4: ( z in dom f & y = f . z ) by FUNCT_1:def 3;
A5: ( dom ({x} --> z) = {x} & rng ({x} --> z) = {z} ) by FUNCOP_1:8, FUNCOP_1:13;
( y = {x} --> z & {z} c= X ) by A1, A4, ZFMISC_1:31;
hence y in Funcs ({x},X) by A5, FUNCT_2:def 2; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Funcs ({x},X) or y in proj2 f )
assume y in Funcs ({x},X) ; :: thesis: y in proj2 f
then consider g being Function such that
A6: y = g and
A7: dom g = {x} and
A8: rng g c= X by FUNCT_2:def 2;
A9: g . x in {(g . x)} by TARSKI:def 1;
A10: rng g = {(g . x)} by A7, FUNCT_1:4;
then g = {x} --> (g . x) by A7, FUNCOP_1:9;
then f . (g . x) = g by A1, A8, A10, A9;
hence y in proj2 f by A1, A6, A8, A10, A9, FUNCT_1:def 3; :: thesis: verum
end;
hence card X = card (Funcs ({x},X)) by CARD_1:5; :: thesis: verum