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):] ) )
deffunc H₁( Function) -> set = [($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 = H₁(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 be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 f or not b₁ in proj1 f or not f . x = f . b₁ or x = b₁ )
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
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

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 A11, A7, A8, ZFMISC_1:33; :: thesis: verum

end;

hence x = y by A9, A10, A5, A6, FUNCT_1:9; :: 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 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
A12: y in dom f and
A13: x = f . y by FUNCT_1:def 5;
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:99;
then A17: rng (g | X2) c= X by A16, XBOOLE_1:1;
rng (g | X1) c= rng g by RELAT_1:99;
then A18: rng (g | X1) c= X by A16, XBOOLE_1:1;
dom (g | X2) = X2 by A15, RELAT_1:91, 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:91, 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:106;
hence x in [:(Funcs X1,X),(Funcs X2,X):] by A1, A12, A13, A14; :: 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 A20: x in [:(Funcs X1,X),(Funcs X2,X):] ; :: thesis: x in proj2 f
then A21: x = [(x `1 ),(x `2 )] by MCART_1:23;
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:18, XBOOLE_1:13;
then A28: rng (g1 +* g2) c= X by XBOOLE_1:1;
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:24
.= x by A2, A21, A22, A23, A25, A26, FUNCT_4:34 ;
hence x in proj2 f by A29, 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