let X, Y, Z be set ; :: thesis: ( Funcs (Z,[:X,Y:]),[:(Funcs (Z,X)),(Funcs (Z,Y)):] are_equipotent & card (Funcs (Z,[:X,Y:])) = card [:(Funcs (Z,X)),(Funcs (Z,Y)):] )
deffunc H1( Function) -> object = [((pr1 (X,Y)) * $1),((pr2 (X,Y)) * $1)];
consider f being Function such that
A1: ( dom f = Funcs (Z,[:X,Y:]) & ( for g being Function st g in Funcs (Z,[:X,Y:]) holds
f . g = H1(g) ) ) from FUNCT_5:sch 1();
 thus Funcs (Z,[:X,Y:]),[:(Funcs (Z,X)),(Funcs (Z,Y)):] are_equipotent :: thesis: card (Funcs (Z,[:X,Y:])) = card [:(Funcs (Z,X)),(Funcs (Z,Y)):]
proof
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = Funcs (Z,[:X,Y:]) & proj2 f = [:(Funcs (Z,X)),(Funcs (Z,Y)):] )
thus f is one-to-one :: thesis: ( proj1 f = Funcs (Z,[:X,Y:]) & proj2 f = [:(Funcs (Z,X)),(Funcs (Z,Y)):] )
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
A2: x1 in dom f and
A3: x2 in dom f and
A4: f . x1 = f . x2 ; :: thesis: x1 = x2
consider g1 being Function such that
A5: x1 = g1 and
A6: dom g1 = Z and
A7: rng g1 c= [:X,Y:] by A1, A2, FUNCT_2:def 2;
consider g2 being Function such that
A8: x2 = g2 and
A9: dom g2 = Z and
A10: rng g2 c= [:X,Y:] by A1, A3, FUNCT_2:def 2;
[((pr1 (X,Y)) * g1),((pr2 (X,Y)) * g1)] = f . x1 by A1, A2, A5
.= [((pr1 (X,Y)) * g2),((pr2 (X,Y)) * g2)] by A1, A3, A4, A8 ;
then A11: ( (pr1 (X,Y)) * g1 = (pr1 (X,Y)) * g2 & (pr2 (X,Y)) * g1 = (pr2 (X,Y)) * g2 ) by XTUPLE_0:1;
now :: thesis: for x being object st x in Z holds
g1 . x = g2 . x
let x be object ; :: thesis: ( x in Z implies g1 . x = g2 . x )
assume A12: x in Z ; :: thesis: g1 . x = g2 . x
then A13: ((pr2 (X,Y)) * g1) . x = (pr2 (X,Y)) . (g1 . x) by A6, FUNCT_1:13;
A14: g2 . x in rng g2 by A9, A12, FUNCT_1:def 3;
then A15: g2 . x = [((g2 . x) `1),((g2 . x) `2)] by A10, MCART_1:21;
A16: g1 . x in rng g1 by A6, A12, FUNCT_1:def 3;
then A17: g1 . x = [((g1 . x) `1),((g1 . x) `2)] by A7, MCART_1:21;
( (g2 . x) `1 in X & (g2 . x) `2 in Y ) by A10, A14, MCART_1:10;
then A18: ( (pr1 (X,Y)) . (((g2 . x) `1),((g2 . x) `2)) = (g2 . x) `1 & (pr2 (X,Y)) . (((g2 . x) `1),((g2 . x) `2)) = (g2 . x) `2 ) by FUNCT_3:def 4, FUNCT_3:def 5;
( (g1 . x) `1 in X & (g1 . x) `2 in Y ) by A7, A16, MCART_1:10;
then A19: ( (pr1 (X,Y)) . (((g1 . x) `1),((g1 . x) `2)) = (g1 . x) `1 & (pr2 (X,Y)) . (((g1 . x) `1),((g1 . x) `2)) = (g1 . x) `2 ) by FUNCT_3:def 4, FUNCT_3:def 5;
( ((pr1 (X,Y)) * g1) . x = (pr1 (X,Y)) . (g1 . x) & ((pr1 (X,Y)) * g2) . x = (pr1 (X,Y)) . (g2 . x) ) by A6, A9, A12, FUNCT_1:13;
hence g1 . x = g2 . x by A9, A11, A12, A13, A17, A15, A19, A18, FUNCT_1:13; :: thesis: verum
end;
hence x1 = x2 by A5, A6, A8, A9, FUNCT_1:2; :: thesis: verum
end;
thus dom f = Funcs (Z,[:X,Y:]) by A1; :: thesis: proj2 f = [:(Funcs (Z,X)),(Funcs (Z,Y)):]
thus rng f c= [:(Funcs (Z,X)),(Funcs (Z,Y)):] :: according to XBOOLE_0:def 10 :: thesis: [:(Funcs (Z,X)),(Funcs (Z,Y)):] c= proj2 f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in [:(Funcs (Z,X)),(Funcs (Z,Y)):] )
assume x in rng f ; :: thesis: x in [:(Funcs (Z,X)),(Funcs (Z,Y)):]
then consider y being object such that
A20: y in dom f and
A21: x = f . y by FUNCT_1:def 3;
consider g being Function such that
A22: y = g and
A23: ( dom g = Z & rng g c= [:X,Y:] ) by A1, A20, FUNCT_2:def 2;
A24: rng ((pr1 (X,Y)) * g) c= X ;
A25: rng ((pr2 (X,Y)) * g) c= Y ;
dom (pr2 (X,Y)) = [:X,Y:] by FUNCT_3:def 5;
then dom ((pr2 (X,Y)) * g) = Z by A23, RELAT_1:27;
then A26: (pr2 (X,Y)) * g in Funcs (Z,Y) by A25, FUNCT_2:def 2;
dom (pr1 (X,Y)) = [:X,Y:] by FUNCT_3:def 4;
then dom ((pr1 (X,Y)) * g) = Z by A23, RELAT_1:27;
then A27: (pr1 (X,Y)) * g in Funcs (Z,X) by A24, FUNCT_2:def 2;
x = [((pr1 (X,Y)) * g),((pr2 (X,Y)) * g)] by A1, A20, A21, A22;
hence x in [:(Funcs (Z,X)),(Funcs (Z,Y)):] by A27, A26, ZFMISC_1:87; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:(Funcs (Z,X)),(Funcs (Z,Y)):] or x in proj2 f )
assume A28: x in [:(Funcs (Z,X)),(Funcs (Z,Y)):] ; :: thesis: x in proj2 f
then A29: x = [(x `1),(x `2)] by MCART_1:21;
x `2 in Funcs (Z,Y) by A28, MCART_1:10;
then consider g2 being Function such that
A30: x `2 = g2 and
A31: dom g2 = Z and
A32: rng g2 c= Y by FUNCT_2:def 2;
x `1 in Funcs (Z,X) by A28, MCART_1:10;
then consider g1 being Function such that
A33: x `1 = g1 and
A34: dom g1 = Z and
A35: rng g1 c= X by FUNCT_2:def 2;
( rng <:g1,g2:> c= [:(rng g1),(rng g2):] & [:(rng g1),(rng g2):] c= [:X,Y:] ) by A35, A32, FUNCT_3:51, ZFMISC_1:96;
then A36: rng <:g1,g2:> c= [:X,Y:] ;
dom <:g1,g2:> = Z /\ Z by A34, A31, FUNCT_3:def 7;
then A37: <:g1,g2:> in Funcs (Z,[:X,Y:]) by A36, FUNCT_2:def 2;
( (pr1 (X,Y)) * <:g1,g2:> = g1 & (pr2 (X,Y)) * <:g1,g2:> = g2 ) by A34, A35, A31, A32, FUNCT_3:52;
then f . <:g1,g2:> = [g1,g2] by A1, A37;
hence x in proj2 f by A1, A29, A33, A30, A37, FUNCT_1:def 3; :: thesis: verum
end;
hence card (Funcs (Z,[:X,Y:])) = card [:(Funcs (Z,X)),(Funcs (Z,Y)):] by CARD_1:5; :: thesis: verum