let x, y, X be set ; :: thesis: ( x <> y implies ( Funcs X,{x,y}, bool X are_equipotent & card (Funcs X,{x,y}) = card (bool X) ) )
assume A1: x <> y ; :: thesis: ( Funcs X,{x,y}, bool X are_equipotent & card (Funcs X,{x,y}) = card (bool X) )
deffunc H₁( Function) -> set = $1 " {x};
consider f being Function such that
A2: ( dom f = Funcs X,{x,y} & ( for g being Function st g in Funcs X,{x,y} holds
f . g = H₁(g) ) ) from FUNCT_5:sch 1();
thus Funcs X,{x,y}, bool X are_equipotent :: thesis: card (Funcs X,{x,y}) = card (bool X)

proof

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = Funcs X,{x,y} & proj2 f = bool X )
thus f is one-to-one :: thesis: ( proj1 f = Funcs X,{x,y} & proj2 f = bool X )

proof

let x1 be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x1 in proj1 f or not b₁ in proj1 f or not f . x1 = f . b₁ or x1 = b₁ )
let x2 be set ; :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume A3: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then consider g1 being Function such that
A4: ( x1 = g1 & dom g1 = X & rng g1 c= {x,y} ) by A2, FUNCT_2:def 2;
consider g2 being Function such that
A5: ( x2 = g2 & dom g2 = X & rng g2 c= {x,y} ) by A2, A3, FUNCT_2:def 2;
A6: ( f . x1 = g1 " {x} & f . x2 = g2 " {x} ) by A2, A3, A4, A5;

now

let z be set ; :: thesis: ( z in X implies g1 . z = g2 . z )
assume A7: z in X ; :: thesis: g1 . z = g2 . z

A8: now

assume A9: g1 . z in {x} ; :: thesis: g1 . z = g2 . z
then z in g2 " {x} by A3, A4, A6, A7, FUNCT_1:def 13;
then g2 . z in {x} by FUNCT_1:def 13;
then ( g2 . z = x & g1 . z = x ) by A9, TARSKI:def 1;
hence g1 . z = g2 . z ; :: thesis: verum

end;

now

assume A10: not g1 . z in {x} ; :: thesis: g1 . z = g2 . z
then not z in g2 " {x} by A3, A6, FUNCT_1:def 13;
then ( not g2 . z in {x} & g1 . z in rng g1 & g2 . z in rng g2 ) by A4, A5, A7, FUNCT_1:def 5, FUNCT_1:def 13;
then ( g2 . z <> x & g1 . z <> x & g1 . z in {x,y} & g2 . z in {x,y} ) by A4, A5, A10, TARSKI:def 1;
then ( g1 . z = y & g2 . z = y ) by TARSKI:def 2;
hence g1 . z = g2 . z ; :: thesis: verum

end;

hence g1 . z = g2 . z by A8; :: thesis: verum

end;

hence x1 = x2 by A4, A5, FUNCT_1:9; :: thesis: verum

end;

thus dom f = Funcs X,{x,y} by A2; :: thesis: proj2 f = bool X
thus rng f c= bool X :: according to XBOOLE_0:def 10 :: thesis: bool X c= proj2 f

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in bool X )
assume z in rng f ; :: thesis: z in bool X
then consider t being set such that
A11: ( t in dom f & z = f . t ) by FUNCT_1:def 5;
consider g being Function such that
A12: ( t = g & dom g = X & rng g c= {x,y} ) by A2, A11, FUNCT_2:def 2;
( z = g " {x} & g " {x} c= X ) by A2, A11, A12, RELAT_1:167;
hence z in bool X ; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in bool X or z in proj2 f )
assume A13: z in bool X ; :: thesis: z in proj2 f
defpred S₁[ set ] means $1 in z;
deffunc H₂( set ) -> set = x;
deffunc H₃( set ) -> set = y;
consider g being Function such that
A14: ( dom g = X & ( for t being set st t in X holds
( ( S₁[t] implies g . t = H₂(t) ) & ( not S₁[t] implies g . t = H₃(t) ) ) ) ) from PARTFUN1:sch 1();
rng g c= {x,y}

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in rng g or t in {x,y} )
assume t in rng g ; :: thesis: t in {x,y}
then consider v being set such that
A15: ( v in dom g & t = g . v ) by FUNCT_1:def 5;
( t = x or t = y ) by A14, A15;
hence t in {x,y} by TARSKI:def 2; :: thesis: verum

end;

then A16: g in Funcs X,{x,y} by A14, FUNCT_2:def 2;
A17: g " {x} = z

proof

thus g " {x} c= z :: according to XBOOLE_0:def 10 :: thesis: z c= g " {x}

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in g " {x} or t in z )
assume t in g " {x} ; :: thesis: t in z
then A18: ( t in dom g & g . t in {x} ) by FUNCT_1:def 13;
then g . t = x by TARSKI:def 1;
hence t in z by A1, A14, A18; :: thesis: verum

end;

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in z or t in g " {x} )
assume A19: t in z ; :: thesis: t in g " {x}
then g . t = x by A13, A14;
then g . t in {x} by TARSKI:def 1;
hence t in g " {x} by A13, A14, A19, FUNCT_1:def 13; :: thesis: verum

end;

f . g = g " {x} by A2, A16;
hence z in proj2 f by A2, A16, A17, FUNCT_1:def 5; :: thesis: verum

end;

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