let X be set ; :: thesis: for x, y being object st x <> y holds
( Funcs (X,{x,y}), bool X are_equipotent & card (Funcs (X,{x,y})) = card (bool X) )
let x, y be object ; :: thesis: ( x <> y implies ( Funcs (X,{x,y}), bool X are_equipotent & card (Funcs (X,{x,y})) = card (bool X) ) )
deffunc H1( Function) -> set = $1 " {x};
consider f being Function such that
A1: ( dom f = Funcs (X,{x,y}) & ( for g being Function st g in Funcs (X,{x,y}) holds
f . g = H1(g) ) ) from FUNCT_5:sch 1();
 assume A2: x <> y ; :: thesis: ( Funcs (X,{x,y}), bool X are_equipotent & card (Funcs (X,{x,y})) = card (bool X) )
thus Funcs (X,{x,y}), bool X are_equipotent :: thesis: card (Funcs (X,{x,y})) = card (bool X)
proof
deffunc H2( object ) -> object = x;
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, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A3: x1 in dom f and
A4: x2 in dom f and
A5: f . x1 = f . x2 ; :: thesis: x1 = x2
consider g2 being Function such that
A6: x2 = g2 and
A7: dom g2 = X and
A8: rng g2 c= {x,y} by A1, A4, FUNCT_2:def 2;
A9: f . x2 = g2 " {x} by A1, A4, A6;
consider g1 being Function such that
A10: x1 = g1 and
A11: dom g1 = X and
A12: rng g1 c= {x,y} by A1, A3, FUNCT_2:def 2;
A13: f . x1 = g1 " {x} by A1, A3, A10;
now :: thesis: for z being object st z in X holds
g1 . z = g2 . z
let z be object ; :: thesis: ( z in X implies g1 . z = g2 . z )
assume A14: z in X ; :: thesis: g1 . z = g2 . z
now :: thesis: ( g1 . z in {x} implies g1 . z = g2 . z )
assume A20: g1 . z in {x} ; :: thesis: g1 . z = g2 . z
then z in g2 " {x} by A5, A11, A13, A9, A14, FUNCT_1:def 7;
then g2 . z in {x} by FUNCT_1:def 7;
then g2 . z = x by TARSKI:def 1;
hence g1 . z = g2 . z by A20, TARSKI:def 1; :: thesis: verum
end;
hence g1 . z = g2 . z by A15; :: thesis: verum
end;
hence x1 = x2 by A10, A11, A6, A7, FUNCT_1:2; :: thesis: verum
end;
thus dom f = Funcs (X,{x,y}) by A1; :: 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 object ; :: 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 object such that
A21: t in dom f and
A22: z = f . t by FUNCT_1:def 3;
consider g being Function such that
A23: t = g and
A24: dom g = X and
rng g c= {x,y} by A1, A21, FUNCT_2:def 2;
A25: g " {x} c= X by A24, RELAT_1:132;
z = g " {x} by A1, A21, A22, A23;
hence z in bool X by A25; :: thesis: verum
end;
deffunc H3( object ) -> object = y;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in bool X or z in proj2 f )
reconsider zz = z as set by TARSKI:1;
defpred S1[ object ] means $1 in zz;
consider g being Function such that
A26: ( dom g = X & ( for t being object st t in X holds
( ( S1[t] implies g . t = H2(t) ) & ( not S1[t] implies g . t = H3(t) ) ) ) ) from PARTFUN1:sch 1();
 assume A27: z in bool X ; :: thesis: z in proj2 f
A28: g " {x} = zz
proof
thus g " {x} c= zz :: according to XBOOLE_0:def 10 :: thesis: zz c= g " {x}
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in g " {x} or t in zz )
assume A29: t in g " {x} ; :: thesis: t in zz
then g . t in {x} by FUNCT_1:def 7;
then A30: g . t = x by TARSKI:def 1;
t in dom g by A29, FUNCT_1:def 7;
hence t in zz by A2, A26, A30; :: thesis: verum
end;
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in zz or t in g " {x} )
assume A31: t in zz ; :: thesis: t in g " {x}
then g . t = x by A27, A26;
then g . t in {x} by TARSKI:def 1;
hence t in g " {x} by A27, A26, A31, FUNCT_1:def 7; :: thesis: verum
end;
rng g c= {x,y}
proof
let t be object ; :: 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 ex v being object st
( v in dom g & t = g . v ) by FUNCT_1:def 3;
then ( t = x or t = y ) by A26;
hence t in {x,y} by TARSKI:def 2; :: thesis: verum
end;
then A32: g in Funcs (X,{x,y}) by A26, FUNCT_2:def 2;
then f . g = g " {x} by A1;
hence z in proj2 f by A1, A32, A28, FUNCT_1:def 3; :: thesis: verum
end;
hence card (Funcs (X,{x,y})) = card (bool X) by CARD_1:5; :: thesis: verum