let X1, X2, X 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):] ) )
assume A1: 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):] )
deffunc H1( Function) -> set = [($1 | X1),($1 | X2)];
consider f being Function such that
A2: ( 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();
 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 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 A3: ( x in dom f & y in dom f ) ; :: thesis: ( not f . x = f . y or x = y )
then consider g1 being Function such that
A4: ( x = g1 & dom g1 = X1 \/ X2 & rng g1 c= X ) by A2, FUNCT_2:def 2;
consider g2 being Function such that
A5: ( y = g2 & dom g2 = X1 \/ X2 & rng g2 c= X ) by A2, A3, FUNCT_2:def 2;
A6: ( f . x = [(g1 | X1),(g1 | X2)] & f . y = [(g2 | X1),(g2 | X2)] ) by A2, A3, A4, A5;
assume A7: f . x = f . y ; :: thesis: x = y
now
let x be set ; :: 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:72;
hence g1 . x = g2 . x by A6, A7, ZFMISC_1:33; :: thesis: verum
end;
hence x = y by A4, A5, FUNCT_1:9; :: thesis: verum
end;
thus dom f = Funcs (X1 \/ X2),X by A2; :: 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 set ; :: 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 set such that
A8: ( y in dom f & x = f . y ) by FUNCT_1:def 5;
consider g being Function such that
A9: ( y = g & dom g = X1 \/ X2 & rng g c= X ) by A2, A8, FUNCT_2:def 2;
( rng (g | X1) c= rng g & rng (g | X2) c= rng g & X1 c= X1 \/ X2 & X2 c= X1 \/ X2 ) by RELAT_1:99, XBOOLE_1:7;
then ( dom (g | X1) = X1 & dom (g | X2) = X2 & rng (g | X1) c= X & rng (g | X2) c= X ) by A9, RELAT_1:91, XBOOLE_1:1;
then ( g | X1 in Funcs X1,X & g | X2 in Funcs X2,X ) by FUNCT_2:def 2;
then [(g | X1),(g | X2)] in [:(Funcs X1,X),(Funcs X2,X):] by ZFMISC_1:106;
hence x in [:(Funcs X1,X),(Funcs X2,X):] by A2, A8, A9; :: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:(Funcs X1,X),(Funcs X2,X):] or x in proj2 f )
assume x in [:(Funcs X1,X),(Funcs X2,X):] ; :: thesis: x in proj2 f
then A10: ( x `1 in Funcs X1,X & x `2 in Funcs X2,X & x = [(x `1 ),(x `2 )] ) by MCART_1:10, MCART_1:23;
then consider g1 being Function such that
A11: ( x `1 = g1 & dom g1 = X1 & rng g1 c= X ) by FUNCT_2:def 2;
consider g2 being Function such that
A12: ( x `2 = g2 & dom g2 = X2 & rng g2 c= X ) by A10, FUNCT_2:def 2;
( rng (g1 +* g2) c= (rng g1) \/ (rng g2) & (rng g1) \/ (rng g2) c= X \/ X & X \/ X = X ) by A11, A12, FUNCT_4:18, XBOOLE_1:13;
then ( dom (g1 +* g2) = X1 \/ X2 & rng (g1 +* g2) c= X ) by A11, A12, FUNCT_4:def 1, XBOOLE_1:1;
then A13: g1 +* g2 in dom f by A2, FUNCT_2:def 2;
then f . (g1 +* g2) = [((g1 +* g2) | X1),((g1 +* g2) | X2)] by A2
.= [((g1 +* g2) | X1),g2] by A12, FUNCT_4:24
.= x by A1, A10, A11, A12, FUNCT_4:34 ;
hence x in proj2 f by A13, FUNCT_1:def 5; :: thesis: verum
end;
hence card (Funcs (X1 \/ X2),X) = card [:(Funcs X1,X),(Funcs X2,X):] by CARD_1:21; :: thesis: verum