let x, y, X be set ; :: thesis: ( x <> y implies ( Funcs {x,y},X,[:X,X:] are_equipotent & card (Funcs {x,y},X) = card [:X,X:] ) )
deffunc H₁( Function) -> set = [($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 = H₁(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

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 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,y} & rng g1 c= X ) by A1, FUNCT_2:def 2;
consider g2 being Function such that
A5: ( x2 = g2 & dom g2 = {x,y} & rng g2 c= X ) by A1, A3, FUNCT_2:def 2;
A6: [(g1 . x),(g1 . y)] = f . x1 by A1, A3, A4
.= [(g2 . x),(g2 . y)] by A1, A3, A5 ;

now

let z be set ; :: 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 A6, ZFMISC_1:33; :: thesis: verum

end;

hence x1 = x2 by A4, A5, FUNCT_1:9; :: 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 set ; :: 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 set such that
A7: ( t in dom f & z = f . t ) by FUNCT_1:def 5;
consider g being Function such that
A8: ( t = g & dom g = {x,y} & rng g c= X ) by A1, A7, FUNCT_2:def 2;
( x in {x,y} & y in {x,y} ) by TARSKI:def 2;
then ( g . x in rng g & g . y in rng g ) by A8, FUNCT_1:def 5;
then ( z = [(g . x),(g . y)] & g . x in X & g . y in X ) by A1, A7, A8;
hence z in [:X,X:] by ZFMISC_1:106; :: thesis: verum

end;

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

proof

let t be set ; :: 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 set st
( a in dom g & t = g . a ) by FUNCT_1:def 5;
hence t in X by A9, A10; :: thesis: verum

end;

then A11: g in Funcs {x,y},X by A10, FUNCT_2:def 2;
( x in {x,y} & y in {x,y} ) by TARSKI:def 2;
then ( g . x = z `1 & g . y = z `2 & f . g = [(g . x),(g . y)] ) by A1, A2, A10, A11;
hence z in proj2 f by A1, A9, A11, FUNCT_1:def 5; :: thesis: verum

end;

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