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 S1[ object , object ] means ( ( $1 in X & $2 = f . $1 ) or ( $1 in X1 & $2 = g . $1 ) );
A9: for x being object st x in X \/ X1 holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in X \/ X1 implies ex y being object st S1[x,y] )
assume x in X \/ X1 ; :: thesis: ex y being object st S1[x,y]
then ( x in X or x in X1 ) by XBOOLE_0:def 3;
hence ex y being object st S1[x,y] ; :: thesis: verum
end;
A10: for x, y, z being object st x in X \/ X1 & S1[x,y] & S1[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 object st x in X \/ X1 holds
S1[x,h . x] from FUNCT_1:sch 2(A10, A9);
 take h ; :: according to WELLORD2:def 4 :: thesis: ( h is one-to-one & dom h = X \/ X1 & rng h = Y \/ Y1 )
thus h is one-to-one :: thesis: ( dom h = X \/ X1 & rng h = Y \/ Y1 )
proof
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom h or not y in dom 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 :: thesis: ( y in X implies not x in X1 )
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 3;
hence contradiction by A1, A2, A15, A17, A16, A19, XBOOLE_0:def 4; :: thesis: verum
end;
now :: thesis: ( x in X implies not y in X1 )
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 3;
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; :: thesis: verum
end;
thus dom h = X \/ X1 by A11; :: thesis: rng h = Y \/ Y1
thus rng h c= Y \/ Y1 :: according to XBOOLE_0:def 10 :: thesis: Y \/ Y1 c= rng h
proof
let x be object ; :: 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 object such that
A21: y in dom h and
A22: x = h . y by FUNCT_1:def 3;
A23: ( ( y in X & x = f . y ) or ( y in X1 & x = g . y ) ) by A11, A12, A21, A22;
A24: now :: thesis: ( y in X1 implies x in Y \/ Y1 )
assume y in X1 ; :: thesis: x in Y \/ Y1
then x in Y1 by A1, A7, A8, A23, FUNCT_1:def 3, XBOOLE_0:def 4;
hence x in Y \/ Y1 by XBOOLE_0:def 3; :: thesis: verum
end;
now :: thesis: ( y in X implies x in Y \/ Y1 )
assume y in X ; :: thesis: x in Y \/ Y1
then x in Y by A1, A4, A5, A23, FUNCT_1:def 3, 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y \/ Y1 or x in rng h )
assume A25: x in Y \/ Y1 ; :: thesis: x in rng h
A26: now :: thesis: ( x in Y1 implies x in rng h )
assume x in Y1 ; :: thesis: x in rng h
then consider y being object such that
A27: y in dom g and
A28: x = g . y by A8, FUNCT_1:def 3;
A29: y in X \/ X1 by A7, A27, XBOOLE_0:def 3;
then S1[y,h . y] by A12;
hence x in rng h by A1, A7, A11, A27, A28, A29, FUNCT_1:def 3, XBOOLE_0:def 4; :: thesis: verum
end;
now :: thesis: ( x in Y implies x in rng h )
assume x in Y ; :: thesis: x in rng h
then consider y being object such that
A30: y in dom f and
A31: x = f . y by A5, FUNCT_1:def 3;
A32: y in X \/ X1 by A4, A30, XBOOLE_0:def 3;
then S1[y,h . y] by A12;
hence x in rng h by A1, A4, A11, A30, A31, A32, FUNCT_1:def 3, XBOOLE_0:def 4; :: thesis: verum
end;
hence x in rng h by A25, A26, XBOOLE_0:def 3; :: thesis: verum