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 that
A1: X1,Y1 are_equipotent and
A2: X2,Y2 are_equipotent ; :: thesis: ( Funcs X1,X2, Funcs Y1,Y2 are_equipotent & card (Funcs X1,X2) = card (Funcs Y1,Y2) )
consider f1 being Function such that
A3: f1 is one-to-one and
A4: dom f1 = Y1 and
A5: rng f1 = X1 by A1, WELLORD2:def 4;
consider f2 being Function such that
A6: f2 is one-to-one and
A7: dom f2 = X2 and
A8: rng f2 = Y2 by A2, WELLORD2:def 4;
Funcs X1,X2, Funcs Y1,Y2 are_equipotent
proof
A9: rng (f1 " ) = Y1 by A3, A4, FUNCT_1:55;
deffunc H1( Function) -> set = f2 * ($1 * f1);
consider F being Function such that
A10: ( dom F = Funcs X1,X2 & ( for g being Function st g in Funcs X1,X2 holds
F . g = H1(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 b1 being set holds
( not x in proj1 F or not b1 in proj1 F or not F . x = F . b1 or x = b1 )
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 that
A11: x in dom F and
A12: y in dom F and
A13: F . x = F . y ; :: thesis: x = y
consider g1 being Function such that
A14: x = g1 and
A15: dom g1 = X1 and
A16: rng g1 c= X2 by A10, A11, FUNCT_2:def 2;
A17: F . x = f2 * (g1 * f1) by A10, A11, A14;
A18: ( rng (g1 * f1) c= X2 & dom (g1 * f1) = Y1 ) by A4, A5, A15, A16, RELAT_1:46, RELAT_1:47;
consider g2 being Function such that
A19: y = g2 and
A20: dom g2 = X1 and
A21: rng g2 c= X2 by A10, A12, FUNCT_2:def 2;
A22: ( rng (g2 * f1) c= X2 & dom (g2 * f1) = Y1 ) by A4, A5, A20, A21, RELAT_1:46, RELAT_1:47;
F . x = f2 * (g2 * f1) by A10, A12, A13, A19;
then A23: g1 * f1 = g2 * f1 by A6, A7, A17, A18, A22, 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 z9 being set such that
A24: ( z9 in Y1 & f1 . z9 = z ) by A4, A5, FUNCT_1:def 5;
thus g1 . z = (g1 * f1) . z9 by A4, A24, FUNCT_1:23
.= g2 . z by A4, A23, A24, FUNCT_1:23 ; :: thesis: verum
end;
hence x = y by A14, A15, A19, A20, FUNCT_1:9; :: thesis: verum
end;
thus dom F = Funcs X1,X2 by A10; :: 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
A25: y in dom F and
A26: x = F . y by FUNCT_1:def 5;
consider g being Function such that
A27: y = g and
A28: ( dom g = X1 & rng g c= X2 ) by A10, A25, FUNCT_2:def 2;
( dom (g * f1) = Y1 & rng (g * f1) c= X2 ) by A4, A5, A28, RELAT_1:46, RELAT_1:47;
then A29: dom (f2 * (g * f1)) = Y1 by A7, RELAT_1:46;
A30: rng (f2 * (g * f1)) c= Y2 by A8, RELAT_1:45;
x = f2 * (g * f1) by A10, A25, A26, A27;
hence x in Funcs Y1,Y2 by A29, A30, 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
A31: x = g and
A32: dom g = Y1 and
A33: rng g c= Y2 by FUNCT_2:def 2;
A34: 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 A6, A8, FUNCT_1:61
.= ((id Y2) * g) * (id Y1) by A3, A4, FUNCT_1:61
.= g * (id Y1) by A33, RELAT_1:79
.= x by A31, A32, RELAT_1:78 ;
dom (f2 " ) = Y2 by A6, A8, FUNCT_1:55;
then A35: dom ((f2 " ) * g) = Y1 by A32, A33, RELAT_1:46;
rng (f2 " ) = X2 by A6, A7, FUNCT_1:55;
then rng ((f2 " ) * g) c= X2 by RELAT_1:45;
then A36: rng (((f2 " ) * g) * (f1 " )) c= X2 by A9, A35, RELAT_1:47;
dom (f1 " ) = X1 by A3, A5, FUNCT_1:55;
then dom (((f2 " ) * g) * (f1 " )) = X1 by A9, A35, RELAT_1:46;
then A37: ((f2 " ) * g) * (f1 " ) in dom F by A10, A36, FUNCT_2:def 2;
then F . (((f2 " ) * g) * (f1 " )) = f2 * ((((f2 " ) * g) * (f1 " )) * f1) by A10;
hence x in proj2 F by A37, A34, 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