let X, X1, Y, Y1 be set ; :: thesis: ( X misses X1 & Y misses Y1 & X,Y are_equipotent & X1,Y1 are_equipotent implies X \/ X1,Y \/ Y1 are_equipotent )
assume that
A1: X /\ X1 = {} and
A2: Y /\ Y1 = {} ; :: according to XBOOLE_0:def 7 :: thesis: ( not X,Y are_equipotent or not X1,Y1 are_equipotent or X \/ X1,Y \/ Y1 are_equipotent )
given f being Function such that A3: f is one-to-one and
A4: dom f = X and
A5: rng f = Y ; :: according to WELLORD2:def 4 :: thesis: ( not X1,Y1 are_equipotent or X \/ X1,Y \/ Y1 are_equipotent )
given g being Function such that A6: g is one-to-one and
A7: dom g = X1 and
A8: rng g = Y1 ; :: according to WELLORD2:def 4 :: thesis: X \/ X1,Y \/ Y1 are_equipotent
defpred S₁[ set , set ] means ( ( $1 in X & $2 = f . $1 ) or ( $1 in X1 & $2 = g . $1 ) );
A9: for x being set st x in X \/ X1 holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in X \/ X1 implies ex y being set st S₁[x,y] )
assume x in X \/ X1 ; :: thesis: ex y being set st S₁[x,y]
then ( x in X or x in X1 ) by XBOOLE_0:def 3;
hence ex y being set st S₁[x,y] ; :: thesis: verum

end;

A10: for x, y, z being set st x in X \/ X1 & S₁[x,y] & S₁[x,z] holds
y = z by A1, XBOOLE_0:def 4;
consider h being Function such that
A11: dom h = X \/ X1 and
A12: for x being set st x in X \/ X1 holds
S₁[x,h . x] from FUNCT_1:sch 2(A10, A9);
take h ; :: according to WELLORD2:def 4 :: thesis: ( h is one-to-one & proj1 h = X \/ X1 & proj2 h = Y \/ Y1 )
thus h is one-to-one :: thesis: ( proj1 h = X \/ X1 & proj2 h = Y \/ Y1 )

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 h or not b₁ in proj1 h or not h . x = h . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 h or not y in proj1 h or not h . x = h . y or x = y )
assume that
A13: x in dom h and
A14: y in dom h and
A15: h . x = h . y ; :: thesis: x = y
A16: ( ( y in X & h . y = f . y ) or ( y in X1 & h . y = g . y ) ) by A11, A12, A14;
A17: ( ( x in X & h . x = f . x ) or ( x in X1 & h . x = g . x ) ) by A11, A12, A13;

A18: now

assume A19: ( y in X & x in X1 ) ; :: thesis: contradiction
then ( f . y in Y & g . x in Y1 ) by A4, A5, A7, A8, FUNCT_1:def 5;
hence contradiction by A1, A2, A15, A17, A16, A19, XBOOLE_0:def 4; :: thesis: verum

end;

now

assume A20: ( x in X & y in X1 ) ; :: thesis: contradiction
then ( f . x in Y & g . y in Y1 ) by A4, A5, A7, A8, FUNCT_1:def 5;
hence contradiction by A1, A2, A15, A17, A16, A20, XBOOLE_0:def 4; :: thesis: verum

end;

hence x = y by A3, A4, A6, A7, A15, A17, A16, A18, FUNCT_1:def 8; :: thesis: verum

end;

thus dom h = X \/ X1 by A11; :: thesis: proj2 h = Y \/ Y1
thus rng h c= Y \/ Y1 :: according to XBOOLE_0:def 10 :: thesis: Y \/ Y1 c= proj2 h

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng h or x in Y \/ Y1 )
assume x in rng h ; :: thesis: x in Y \/ Y1
then consider y being set such that
A21: y in dom h and
A22: x = h . y by FUNCT_1:def 5;
A23: ( ( y in X & x = f . y ) or ( y in X1 & x = g . y ) ) by A11, A12, A21, A22;

A24: now

assume y in X1 ; :: thesis: x in Y \/ Y1
then x in Y1 by A1, A7, A8, A23, FUNCT_1:def 5, XBOOLE_0:def 4;
hence x in Y \/ Y1 by XBOOLE_0:def 3; :: thesis: verum

end;

now

assume y in X ; :: thesis: x in Y \/ Y1
then x in Y by A1, A4, A5, A23, FUNCT_1:def 5, XBOOLE_0:def 4;
hence x in Y \/ Y1 by XBOOLE_0:def 3; :: thesis: verum

end;

hence x in Y \/ Y1 by A11, A21, A24, XBOOLE_0:def 3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y \/ Y1 or x in proj2 h )
assume A25: x in Y \/ Y1 ; :: thesis: x in proj2 h

A26: now

assume x in Y1 ; :: thesis: x in proj2 h
then consider y being set such that
A27: y in dom g and
A28: x = g . y by A8, FUNCT_1:def 5;
A29: y in X \/ X1 by A7, A27, XBOOLE_0:def 3;
then S₁[y,h . y] by A12;
hence x in proj2 h by A1, A7, A11, A27, A28, A29, FUNCT_1:def 5, XBOOLE_0:def 4; :: thesis: verum

end;

now

assume x in Y ; :: thesis: x in proj2 h
then consider y being set such that
A30: y in dom f and
A31: x = f . y by A5, FUNCT_1:def 5;
A32: y in X \/ X1 by A4, A30, XBOOLE_0:def 3;
then S₁[y,h . y] by A12;
hence x in proj2 h by A1, A4, A11, A30, A31, A32, FUNCT_1:def 5, XBOOLE_0:def 4; :: thesis: verum

end;

hence x in proj2 h by A25, A26, XBOOLE_0:def 3; :: thesis: verum