let X1, X2, Y1, 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;
Funcs (X1,X2), Funcs (Y1,Y2) are_equipotent
proof
A9: rng (f1 ") = Y1 by A3, A4, FUNCT_1:33;
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, y be object ; :: according to FUNCT_1:def 4 :: 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:27, RELAT_1:28;
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:27, RELAT_1:28;
F . x = f2 * (g2 * f1) by A10, A12, A13, A19;
then A23: g1 * f1 = g2 * f1 by A6, A7, A17, A18, A22, FUNCT_1:27;
now :: thesis: for z being object st z in X1 holds
g1 . z = g2 . z
let z be object ; :: thesis: ( z in X1 implies g1 . z = g2 . z )
assume z in X1 ; :: thesis: g1 . z = g2 . z
then consider z9 being object such that
A24: ( z9 in Y1 & f1 . z9 = z ) by A4, A5, FUNCT_1:def 3;
thus g1 . z = (g1 * f1) . z9 by A4, A24, FUNCT_1:13
.= g2 . z by A4, A23, A24, FUNCT_1:13 ; :: thesis: verum
end;
hence x = y by A14, A15, A19, A20, FUNCT_1:2; :: 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 object ; :: 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 object such that
A25: y in dom F and
A26: x = F . y by FUNCT_1:def 3;
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:27, RELAT_1:28;
then A29: dom (f2 * (g * f1)) = Y1 by A7, RELAT_1:27;
A30: rng (f2 * (g * f1)) c= Y2 by A8, RELAT_1:26;
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 object ; :: 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:36
.= (f2 * ((f2 ") * g)) * ((f1 ") * f1) by RELAT_1:36
.= ((f2 * (f2 ")) * g) * ((f1 ") * f1) by RELAT_1:36
.= ((id Y2) * g) * ((f1 ") * f1) by A6, A8, FUNCT_1:39
.= ((id Y2) * g) * (id Y1) by A3, A4, FUNCT_1:39
.= g * (id Y1) by A33, RELAT_1:53
.= x by A31, A32, RELAT_1:52 ;
dom (f2 ") = Y2 by A6, A8, FUNCT_1:33;
then A35: dom ((f2 ") * g) = Y1 by A32, A33, RELAT_1:27;
rng (f2 ") = X2 by A6, A7, FUNCT_1:33;
then rng ((f2 ") * g) c= X2 by RELAT_1:26;
then A36: rng (((f2 ") * g) * (f1 ")) c= X2 by A9, A35, RELAT_1:28;
dom (f1 ") = X1 by A3, A5, FUNCT_1:33;
then dom (((f2 ") * g) * (f1 ")) = X1 by A9, A35, RELAT_1:27;
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 3; :: thesis: verum
end;
hence ( Funcs (X1,X2), Funcs (Y1,Y2) are_equipotent & card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) ) by CARD_1:5; :: thesis: verum