let X1, Y1, X2, Y2 be set ; :: thesis: ( X1,Y1 are_equipotent & X2,Y2 are_equipotent implies ( Funcs X1,X2, Funcs Y1,Y2 are_equipotent & card (Funcs X1,X2) = card (Funcs Y1,Y2) ) )
assume A1: ( X1,Y1 are_equipotent & X2,Y2 are_equipotent ) ; :: thesis: ( Funcs X1,X2, Funcs Y1,Y2 are_equipotent & card (Funcs X1,X2) = card (Funcs Y1,Y2) )
then consider f1 being Function such that
A2: ( f1 is one-to-one & dom f1 = Y1 & rng f1 = X1 ) by WELLORD2:def 4;
consider f2 being Function such that
A3: ( f2 is one-to-one & dom f2 = X2 & rng f2 = Y2 ) by A1, WELLORD2:def 4;
Funcs X1,X2, Funcs Y1,Y2 are_equipotent

proof

deffunc H₁( Function) -> set = f2 * ($1 * f1);
consider F being Function such that
A4: ( dom F = Funcs X1,X2 & ( for g being Function st g in Funcs X1,X2 holds
F . g = H₁(g) ) ) from FUNCT_5:sch 1();
take F ; :: according to WELLORD2:def 4 :: thesis: ( F is one-to-one & proj1 F = Funcs X1,X2 & proj2 F = Funcs Y1,Y2 )
thus F is one-to-one :: thesis: ( proj1 F = Funcs X1,X2 & proj2 F = Funcs Y1,Y2 )

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 F or not b₁ in proj1 F or not F . x = F . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 F or not y in proj1 F or not F . x = F . y or x = y )
assume A5: ( x in dom F & y in dom F & F . x = F . y ) ; :: thesis: x = y
then consider g1 being Function such that
A6: ( x = g1 & dom g1 = X1 & rng g1 c= X2 ) by A4, FUNCT_2:def 2;
consider g2 being Function such that
A7: ( y = g2 & dom g2 = X1 & rng g2 c= X2 ) by A4, A5, FUNCT_2:def 2;
( F . x = f2 * (g1 * f1) & F . x = f2 * (g2 * f1) & rng (g1 * f1) c= X2 & rng (g2 * f1) c= X2 & dom (g1 * f1) = Y1 & dom (g2 * f1) = Y1 ) by A2, A4, A5, A6, A7, RELAT_1:46, RELAT_1:47;
then A8: g1 * f1 = g2 * f1 by A3, FUNCT_1:49;

now

let z be set ; :: thesis: ( z in X1 implies g1 . z = g2 . z )
assume z in X1 ; :: thesis: g1 . z = g2 . z
then consider z' being set such that
A9: ( z' in Y1 & f1 . z' = z ) by A2, FUNCT_1:def 5;
thus g1 . z = (g1 * f1) . z' by A2, A9, FUNCT_1:23
.= g2 . z by A2, A8, A9, FUNCT_1:23 ; :: thesis: verum

end;

hence x = y by A6, A7, FUNCT_1:9; :: thesis: verum

end;

thus dom F = Funcs X1,X2 by A4; :: thesis: proj2 F = Funcs Y1,Y2
thus rng F c= Funcs Y1,Y2 :: according to XBOOLE_0:def 10 :: thesis: Funcs Y1,Y2 c= proj2 F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F or x in Funcs Y1,Y2 )
assume x in rng F ; :: thesis: x in Funcs Y1,Y2
then consider y being set such that
A10: ( y in dom F & x = F . y ) by FUNCT_1:def 5;
consider g being Function such that
A11: ( y = g & dom g = X1 & rng g c= X2 ) by A4, A10, FUNCT_2:def 2;
( dom (g * f1) = Y1 & rng (g * f1) c= X2 ) by A2, A11, RELAT_1:46, RELAT_1:47;
then ( x = f2 * (g * f1) & dom (f2 * (g * f1)) = Y1 & rng (f2 * (g * f1)) c= Y2 ) by A3, A4, A10, A11, RELAT_1:45, RELAT_1:46;
hence x in Funcs Y1,Y2 by FUNCT_2:def 2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Funcs Y1,Y2 or x in proj2 F )
assume x in Funcs Y1,Y2 ; :: thesis: x in proj2 F
then consider g being Function such that
A12: ( x = g & dom g = Y1 & rng g c= Y2 ) by FUNCT_2:def 2;
A13: ( rng (f1 " ) = Y1 & dom (f1 " ) = X1 & dom (f2 " ) = Y2 & rng (f2 " ) = X2 ) by A2, A3, FUNCT_1:55;
then ( dom ((f2 " ) * g) = Y1 & rng ((f2 " ) * g) c= X2 & rng (((f2 " ) * g) * (f1 " )) c= rng ((f2 " ) * g) ) by A12, RELAT_1:45, RELAT_1:46;
then ( dom (((f2 " ) * g) * (f1 " )) = X1 & rng (((f2 " ) * g) * (f1 " )) c= X2 ) by A13, RELAT_1:46, RELAT_1:47;
then A14: ((f2 " ) * g) * (f1 " ) in dom F by A4, FUNCT_2:def 2;
then A15: F . (((f2 " ) * g) * (f1 " )) = f2 * ((((f2 " ) * g) * (f1 " )) * f1) by A4;
f2 * ((((f2 " ) * g) * (f1 " )) * f1) = f2 * (((f2 " ) * g) * ((f1 " ) * f1)) by RELAT_1:55
.= (f2 * ((f2 " ) * g)) * ((f1 " ) * f1) by RELAT_1:55
.= ((f2 * (f2 " )) * g) * ((f1 " ) * f1) by RELAT_1:55
.= ((id Y2) * g) * ((f1 " ) * f1) by A3, FUNCT_1:61
.= ((id Y2) * g) * (id Y1) by A2, FUNCT_1:61
.= g * (id Y1) by A12, RELAT_1:79
.= x by A12, RELAT_1:78 ;
hence x in proj2 F by A14, A15, FUNCT_1:def 5; :: thesis: verum

end;

hence ( Funcs X1,X2, Funcs Y1,Y2 are_equipotent & card (Funcs X1,X2) = card (Funcs Y1,Y2) ) by CARD_1:21; :: thesis: verum