let A, B be Ordinal; :: thesis: for x1, x2 being object st x1 <> x2 holds
( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) )
let x1, x2 be object ; :: thesis: ( x1 <> x2 implies ( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) ) )
defpred S₁[ set ] means $1 in A;
deffunc H₂( set ) -> object = [$1,x1];
deffunc H₃( Ordinal) -> object = [($1 -^ A),x2];
consider f being Function such that
A1: dom f = A +^ B and
A2: for x being Ordinal st x in A +^ B holds
( ( S₁[x] implies f . x = H₂(x) ) & ( not S₁[x] implies f . x = H₃(x) ) ) from FINSET_1:sch 1();
assume A3: x1 <> x2 ; :: thesis: ( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) )
thus A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent :: thesis: card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:])

proof

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = A +^ B & proj2 f = [:A,{x1}:] \/ [:B,{x2}:] )
thus f is one-to-one :: thesis: ( proj1 f = A +^ B & proj2 f = [:A,{x1}:] \/ [:B,{x2}:] )

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
A4: ( x in dom f & y in dom f ) and
A5: f . x = f . y ; :: thesis: x = y
reconsider C1 = x, C2 = y as Ordinal by A1, A4;

per cases ( ( x in A & y in A ) or ( not x in A & not y in A ) or ( x in A & not y in A ) or ( not x in A & y in A ) ) ;

suppose A6: ( x in A & y in A ) ; :: thesis: x = y

A7: ( [x,x1] `1 = C1 & [y,x1] `1 = C2 ) ;
( f . C1 = [x,x1] & f . C2 = [y,x1] ) by A1, A2, A4, A6;
hence x = y by A5, A7; :: thesis: verum

end;

suppose A8: ( not x in A & not y in A ) ; :: thesis: x = y

A9: ( [(C1 -^ A),x2] `1 = C1 -^ A & [(C2 -^ A),x2] `1 = C2 -^ A ) ;
( f . x = [(C1 -^ A),x2] & f . y = [(C2 -^ A),x2] ) by A1, A2, A4, A8;
then A10: C1 -^ A = C2 -^ A by A5, A9;
A c= C1 by A8, ORDINAL1:16;
then A11: C1 = A +^ (C1 -^ A) by ORDINAL3:def 5;
A c= C2 by A8, ORDINAL1:16;
hence x = y by A10, A11, ORDINAL3:def 5; :: thesis: verum

end;

suppose A12: ( x in A & not y in A ) ; :: thesis: x = y

A13: ( [x,x1] `2 = x1 & [(C2 -^ A),x2] `2 = x2 ) ;
( f . x = [x,x1] & f . y = [(C2 -^ A),x2] ) by A1, A2, A4, A12;
hence x = y by A3, A5, A13; :: thesis: verum

end;

suppose A14: ( not x in A & y in A ) ; :: thesis: x = y

A15: ( [y,x1] `2 = x1 & [(C1 -^ A),x2] `2 = x2 ) ;
( f . y = [y,x1] & f . x = [(C1 -^ A),x2] ) by A1, A2, A4, A14;
hence x = y by A3, A5, A15; :: thesis: verum

end;

end;

end;

thus dom f = A +^ B by A1; :: thesis: proj2 f = [:A,{x1}:] \/ [:B,{x2}:]
thus rng f c= [:A,{x1}:] \/ [:B,{x2}:] :: according to XBOOLE_0:def 10 :: thesis: [:A,{x1}:] \/ [:B,{x2}:] c= proj2 f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in [:A,{x1}:] \/ [:B,{x2}:] )
A16: x1 in {x1} by TARSKI:def 1;
A17: x2 in {x2} by TARSKI:def 1;
assume x in rng f ; :: thesis: x in [:A,{x1}:] \/ [:B,{x2}:]
then consider y being object such that
A18: y in dom f and
A19: x = f . y by FUNCT_1:def 3;
reconsider C = y as Ordinal by A1, A18;

per cases ( y in A or not y in A ) ;

suppose y in A ; :: thesis: x in [:A,{x1}:] \/ [:B,{x2}:]

then ( x = [C,x1] & [C,x1] in [:A,{x1}:] ) by A1, A2, A18, A19, A16, ZFMISC_1:87;
hence x in [:A,{x1}:] \/ [:B,{x2}:] by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A20: not y in A ; :: thesis: x in [:A,{x1}:] \/ [:B,{x2}:]

then A c= C by ORDINAL1:16;
then A +^ (C -^ A) = C by ORDINAL3:def 5;
then C -^ A in B by A1, A18, ORDINAL3:22;
then A21: [(C -^ A),x2] in [:B,{x2}:] by A17, ZFMISC_1:87;
x = [(C -^ A),x2] by A1, A2, A18, A19, A20;
hence x in [:A,{x1}:] \/ [:B,{x2}:] by A21, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:A,{x1}:] \/ [:B,{x2}:] or x in proj2 f )
assume A22: x in [:A,{x1}:] \/ [:B,{x2}:] ; :: thesis: x in proj2 f

A23: now :: thesis: ( x in [:B,{x2}:] implies x in proj2 f )

assume x in [:B,{x2}:] ; :: thesis: x in proj2 f
then consider y, z being object such that
A24: y in B and
A25: z in {x2} and
A26: x = [y,z] by ZFMISC_1:84;
reconsider y = y as Ordinal by A24;
A27: A +^ y in A +^ B by A24, ORDINAL2:32;
A28: not A +^ y in A by ORDINAL1:5, ORDINAL3:24;
( (A +^ y) -^ A = y & z = x2 ) by A25, ORDINAL3:52, TARSKI:def 1;
then x = f . (A +^ y) by A2, A26, A27, A28;
hence x in proj2 f by A1, A27, FUNCT_1:def 3; :: thesis: verum

end;

now :: thesis: ( x in [:A,{x1}:] implies x in proj2 f )

assume x in [:A,{x1}:] ; :: thesis: x in proj2 f
then consider y, z being object such that
A29: y in A and
A30: z in {x1} and
A31: x = [y,z] by ZFMISC_1:84;
A32: A c= A +^ B by ORDINAL3:24;
z = x1 by A30, TARSKI:def 1;
then x = f . y by A2, A29, A31, A32;
hence x in proj2 f by A1, A29, A32, FUNCT_1:def 3; :: thesis: verum

end;

hence x in proj2 f by A22, A23, XBOOLE_0:def 3; :: thesis: verum

end;

hence card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) by CARD_1:5; :: thesis: verum