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