let X be set ; :: thesis: for x, y being object st x <> y holds
( Funcs ({x,y},X),[:X,X:] are_equipotent & card (Funcs ({x,y},X)) = card [:X,X:] )
let x, y be object ; :: thesis: ( x <> y implies ( Funcs ({x,y},X),[:X,X:] are_equipotent & card (Funcs ({x,y},X)) = card [:X,X:] ) )
deffunc H1( Function) -> object = [($1 . x),($1 . y)];
consider f being Function such that
A1: ( dom f = Funcs ({x,y},X) & ( for g being Function st g in Funcs ({x,y},X) holds
f . g = H1(g) ) ) from FUNCT_5:sch 1();
 assume A2: x <> y ; :: thesis: ( Funcs ({x,y},X),[:X,X:] are_equipotent & card (Funcs ({x,y},X)) = card [:X,X:] )
thus Funcs ({x,y},X),[:X,X:] are_equipotent :: thesis: card (Funcs ({x,y},X)) = card [:X,X:]
proof
defpred S1[ object ] means $1 = x;
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = Funcs ({x,y},X) & proj2 f = [:X,X:] )
thus f is one-to-one :: thesis: ( proj1 f = Funcs ({x,y},X) & proj2 f = [:X,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,y} and
rng g2 c= X by A1, A4, FUNCT_2:def 2;
consider g1 being Function such that
A8: x1 = g1 and
A9: dom g1 = {x,y} and
rng g1 c= X by A1, A3, FUNCT_2:def 2;
A10: [(g1 . x),(g1 . y)] = f . x1 by A1, A3, A8
.= [(g2 . x),(g2 . y)] by A1, A4, A5, A6 ;
now :: thesis: for z being object st z in {x,y} holds
g1 . z = g2 . z
let z be object ; :: thesis: ( z in {x,y} implies g1 . z = g2 . z )
assume z in {x,y} ; :: thesis: g1 . z = g2 . z
then ( z = x or z = y ) by TARSKI:def 2;
hence g1 . z = g2 . z by A10, XTUPLE_0:1; :: thesis: verum
end;
hence x1 = x2 by A8, A9, A6, A7, FUNCT_1:2; :: thesis: verum
end;
thus dom f = Funcs ({x,y},X) by A1; :: thesis: proj2 f = [:X,X:]
thus rng f c= [:X,X:] :: according to XBOOLE_0:def 10 :: thesis: [:X,X:] c= proj2 f
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in [:X,X:] )
assume z in rng f ; :: thesis: z in [:X,X:]
then consider t being object such that
A11: t in dom f and
A12: z = f . t by FUNCT_1:def 3;
consider g being Function such that
A13: t = g and
A14: dom g = {x,y} and
A15: rng g c= X by A1, A11, FUNCT_2:def 2;
x in {x,y} by TARSKI:def 2;
then A16: g . x in rng g by A14, FUNCT_1:def 3;
y in {x,y} by TARSKI:def 2;
then A17: g . y in rng g by A14, FUNCT_1:def 3;
z = [(g . x),(g . y)] by A1, A11, A12, A13;
hence z in [:X,X:] by A15, A16, A17, ZFMISC_1:87; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in [:X,X:] or z in proj2 f )
deffunc H2( object ) -> object = z `1 ;
deffunc H3( object ) -> object = z `2 ;
consider g being Function such that
A18: ( dom g = {x,y} & ( for t being object st t in {x,y} holds
( ( S1[t] implies g . t = H2(t) ) & ( not S1[t] implies g . t = H3(t) ) ) ) ) from PARTFUN1:sch 1();
 x in {x,y} by TARSKI:def 2;
then A19: g . x = z `1 by A18;
y in {x,y} by TARSKI:def 2;
then A20: g . y = z `2 by A2, A18;
assume A21: z in [:X,X:] ; :: thesis: z in proj2 f
then A22: z = [(z `1),(z `2)] by MCART_1:21;
A23: ( z `1 in X & z `2 in X ) by A21, MCART_1:10;
rng g c= X
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng g or t in X )
assume t in rng g ; :: thesis: t in X
then ex a being object st
( a in dom g & t = g . a ) by FUNCT_1:def 3;
hence t in X by A23, A18; :: thesis: verum
end;
then A24: g in Funcs ({x,y},X) by A18, FUNCT_2:def 2;
then f . g = [(g . x),(g . y)] by A1;
hence z in proj2 f by A1, A22, A24, A19, A20, FUNCT_1:def 3; :: thesis: verum
end;
hence card (Funcs ({x,y},X)) = card [:X,X:] by CARD_1:5; :: thesis: verum