let X, x be set ; :: thesis: ( X, Funcs {x},X are_equipotent & card X = card (Funcs {x},X) )
deffunc H₁( set ) -> Element of bool [:{x},{$1}:] = {x} --> $1;
consider f being Function such that
A1: ( dom f = X & ( for y being set st y in X holds
f . y = H₁(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 be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not y in proj1 f or not b₁ in proj1 f or not f . y = f . b₁ or y = b₁ )
let z be set ; :: 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:13;
hence ( not f . y = f . z or y = z ) by A2, A3, FUNCOP_1:13; :: 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 set ; :: 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 set such that
A4: ( z in dom f & y = f . z ) by FUNCT_1:def 5;
A5: ( dom ({x} --> z) = {x} & rng ({x} --> z) = {z} ) by FUNCOP_1:14, FUNCOP_1:19;
( y = {x} --> z & {z} c= X ) by A1, A4, ZFMISC_1:37;
hence y in Funcs {x},X by A5, FUNCT_2:def 2; :: thesis: verum

end;

let y be set ; :: 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:14;
then g = {x} --> (g . x) by A7, FUNCOP_1:15;
then f . (g . x) = g by A1, A8, A10, A9;
hence y in proj2 f by A1, A6, A8, A10, A9, FUNCT_1:def 5; :: thesis: verum

end;

hence card X = card (Funcs {x},X) by CARD_1:21; :: thesis: verum