let X be set ; :: thesis: for S1, S2 being finite Subset of X
for R being connected Order of X holds
( order ((S1 \/ S2),R) = (order (S1,R)) ^ (order (S2,R)) iff for x, y being set st x in S1 & y in S2 holds
( x <> y & x,y in R ) )
let S1, S2 be finite Subset of X; :: thesis: for R being connected Order of X holds
( order ((S1 \/ S2),R) = (order (S1,R)) ^ (order (S2,R)) iff for x, y being set st x in S1 & y in S2 holds
( x <> y & x,y in R ) )
let R be connected Order of X; :: thesis: ( order ((S1 \/ S2),R) = (order (S1,R)) ^ (order (S2,R)) iff for x, y being set st x in S1 & y in S2 holds
( x <> y & x,y in R ) )
A1: ( rng (order ((S1 \/ S2),R)) = S1 \/ S2 & rng (order (S1,R)) = S1 & rng (order (S2,R)) = S2 ) by Def11;
A2: dom ((order (S1,R)) ^ (order (S2,R))) = (dom (order (S1,R))) +^ (dom (order (S2,R))) by ORDINAL4:def 1;
A3: ( order ((S1 \/ S2),R) is one-to-one & order (S1,R) is one-to-one & order (S2,R) is one-to-one ) by Def11;

hereby :: thesis: ( ( for x, y being set st x in S1 & y in S2 holds
( x <> y & x,y in R ) ) implies order ((S1 \/ S2),R) = (order (S1,R)) ^ (order (S2,R)) )

assume A4: order ((S1 \/ S2),R) = (order (S1,R)) ^ (order (S2,R)) ; :: thesis: for x, y being set st x in S1 & y in S2 holds
( x <> y & x,y in R )
let x, y be set ; :: thesis: ( x in S1 & y in S2 implies ( x <> y & x,y in R ) )
assume A5: ( x in S1 & y in S2 ) ; :: thesis: ( x <> y & x,y in R )
then consider z being object such that
A6: ( z in dom (order (S1,R)) & x = (order (S1,R)) . z ) by A1, FUNCT_1:def 3;
consider s being object such that
A7: ( s in dom (order (S2,R)) & y = (order (S2,R)) . s ) by A1, A5, FUNCT_1:def 3;
reconsider z = z, s = s as Element of NAT by A6, A7;
A8: ( (order ((S1 \/ S2),R)) . z = x & (order ((S1 \/ S2),R)) . ((dom (order (S1,R))) +^ s) = y ) by A4, A6, A7, ORDINAL4:def 1;
A9: ( z in dom (order ((S1 \/ S2),R)) & (dom (order (S1,R))) +^ s in dom (order ((S1 \/ S2),R)) ) by A2, A6, A7, A4, ORDINAL3:17, ORDINAL3:25;
A10: (dom (order (S1,R))) +^ s = Segm ((dom (order (S1,R))) + s) by CARD_2:36;
z in (dom (order (S1,R))) +^ s by A6, ORDINAL3:25;
then z < (dom (order (S1,R))) + s by A10, NAT_1:44;
hence ( x <> y & x,y in R ) by A3, A8, A9, A10, Def11; :: thesis: verum

end;

assume A11: for x, y being set st x in S1 & y in S2 holds
( x <> y & x,y in R ) ; :: thesis: order ((S1 \/ S2),R) = (order (S1,R)) ^ (order (S2,R))
A12: rng ((order (S1,R)) ^ (order (S2,R))) = S1 \/ S2 by A1, Th7;
set o1 = order (S1,R);
set o2 = order (S2,R);
A13: (order (S1,R)) ^ (order (S2,R)) is one-to-one

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom ((order (S1,R)) ^ (order (S2,R))) or not y in dom ((order (S1,R)) ^ (order (S2,R))) or not ((order (S1,R)) ^ (order (S2,R))) . x = ((order (S1,R)) ^ (order (S2,R))) . y or x = y )
assume A14: ( x in dom ((order (S1,R)) ^ (order (S2,R))) & y in dom ((order (S1,R)) ^ (order (S2,R))) & ((order (S1,R)) ^ (order (S2,R))) . x = ((order (S1,R)) ^ (order (S2,R))) . y ) ; :: thesis: x = y

per cases ( ( x in dom (order (S1,R)) & y in dom (order (S1,R)) ) or ( x in dom (order (S1,R)) & ex a being Ordinal st
( a in dom (order (S2,R)) & y = (dom (order (S1,R))) +^ a ) ) or ( y in dom (order (S1,R)) & ex a being Ordinal st
( a in dom (order (S2,R)) & x = (dom (order (S1,R))) +^ a ) ) or ( ex a being Ordinal st
( a in dom (order (S2,R)) & x = (dom (order (S1,R))) +^ a ) & ex a being Ordinal st
( a in dom (order (S2,R)) & y = (dom (order (S1,R))) +^ a ) ) ) by A14, A2, ORDINAL3:38;

suppose A15: ( x in dom (order (S1,R)) & y in dom (order (S1,R)) ) ; :: thesis: x = y

then ( ((order (S1,R)) ^ (order (S2,R))) . x = (order (S1,R)) . x & ((order (S1,R)) ^ (order (S2,R))) . y = (order (S1,R)) . y ) by ORDINAL4:def 1;
hence x = y by A3, A14, A15; :: thesis: verum

end;

suppose A16: ( x in dom (order (S1,R)) & ex a being Ordinal st
( a in dom (order (S2,R)) & y = (dom (order (S1,R))) +^ a ) ) ; :: thesis: x = y

then consider a being Ordinal such that
A17: ( a in dom (order (S2,R)) & y = (dom (order (S1,R))) +^ a ) ;
( ((order (S1,R)) ^ (order (S2,R))) . x = (order (S1,R)) . x & ((order (S1,R)) ^ (order (S2,R))) . y = (order (S2,R)) . a ) by A16, A17, ORDINAL4:def 1;
then ( ((order (S1,R)) ^ (order (S2,R))) . x in S1 & ((order (S1,R)) ^ (order (S2,R))) . y in S2 ) by A1, A16, A17, FUNCT_1:def 3;
hence x = y by A11, A14; :: thesis: verum

end;

suppose A18: ( y in dom (order (S1,R)) & ex a being Ordinal st
( a in dom (order (S2,R)) & x = (dom (order (S1,R))) +^ a ) ) ; :: thesis: x = y

then consider a being Ordinal such that
A19: ( a in dom (order (S2,R)) & x = (dom (order (S1,R))) +^ a ) ;
( ((order (S1,R)) ^ (order (S2,R))) . y = (order (S1,R)) . y & ((order (S1,R)) ^ (order (S2,R))) . x = (order (S2,R)) . a ) by A18, A19, ORDINAL4:def 1;
then ( ((order (S1,R)) ^ (order (S2,R))) . x in S2 & ((order (S1,R)) ^ (order (S2,R))) . y in S1 ) by A1, A18, A19, FUNCT_1:def 3;
hence x = y by A11, A14; :: thesis: verum

end;

suppose A20: ( ex a being Ordinal st
( a in dom (order (S2,R)) & x = (dom (order (S1,R))) +^ a ) & ex a being Ordinal st
( a in dom (order (S2,R)) & y = (dom (order (S1,R))) +^ a ) ) ; :: thesis: x = y

then consider a being Ordinal such that
A21: ( a in dom (order (S2,R)) & x = (dom (order (S1,R))) +^ a ) ;
consider b being Ordinal such that
A22: ( b in dom (order (S2,R)) & y = (dom (order (S1,R))) +^ b ) by A20;
( ((order (S1,R)) ^ (order (S2,R))) . x = (order (S2,R)) . a & ((order (S1,R)) ^ (order (S2,R))) . y = (order (S2,R)) . b ) by A21, A22, ORDINAL4:def 1;
hence x = y by A21, A22, A3, A14; :: thesis: verum

end;

end;

end;

now :: thesis: for x, y being Nat st x in dom ((order (S1,R)) ^ (order (S2,R))) & y in dom ((order (S1,R)) ^ (order (S2,R))) holds
( x <= y iff ((order (S1,R)) ^ (order (S2,R))) . x,((order (S1,R)) ^ (order (S2,R))) . y in R )

let x, y be Nat; :: thesis: ( x in dom ((order (S1,R)) ^ (order (S2,R))) & y in dom ((order (S1,R)) ^ (order (S2,R))) implies ( b₁ <= b₂ iff ((order (S1,R)) ^ (order (S2,R))) . b₁,((order (S1,R)) ^ (order (S2,R))) . b₂ in R ) )
assume A23: ( x in dom ((order (S1,R)) ^ (order (S2,R))) & y in dom ((order (S1,R)) ^ (order (S2,R))) ) ; :: thesis: ( b₁ <= b₂ iff ((order (S1,R)) ^ (order (S2,R))) . b₁,((order (S1,R)) ^ (order (S2,R))) . b₂ in R )

per cases ( ( x in dom (order (S1,R)) & y in dom (order (S1,R)) ) or ( x in dom (order (S1,R)) & ex a being Ordinal st
( a in dom (order (S2,R)) & y = (dom (order (S1,R))) +^ a ) ) or ( y in dom (order (S1,R)) & ex a being Ordinal st
( a in dom (order (S2,R)) & x = (dom (order (S1,R))) +^ a ) ) or ( ex a being Ordinal st
( a in dom (order (S2,R)) & x = (dom (order (S1,R))) +^ a ) & ex a being Ordinal st
( a in dom (order (S2,R)) & y = (dom (order (S1,R))) +^ a ) ) ) by A23, A2, ORDINAL3:38;

suppose A24: ( x in dom (order (S1,R)) & y in dom (order (S1,R)) ) ; :: thesis: ( b₁ <= b₂ iff ((order (S1,R)) ^ (order (S2,R))) . b₁,((order (S1,R)) ^ (order (S2,R))) . b₂ in R )

then ( ((order (S1,R)) ^ (order (S2,R))) . x = (order (S1,R)) . x & ((order (S1,R)) ^ (order (S2,R))) . y = (order (S1,R)) . y ) by ORDINAL4:def 1;
hence ( x <= y iff ((order (S1,R)) ^ (order (S2,R))) . x,((order (S1,R)) ^ (order (S2,R))) . y in R ) by A24, Def11; :: thesis: verum

end;

suppose A25: ( x in dom (order (S1,R)) & ex a being Ordinal st
( a in dom (order (S2,R)) & y = (dom (order (S1,R))) +^ a ) ) ; :: thesis: ( b₁ <= b₂ iff ((order (S1,R)) ^ (order (S2,R))) . b₁,((order (S1,R)) ^ (order (S2,R))) . b₂ in R )

then consider a being Ordinal such that
A26: ( a in dom (order (S2,R)) & y = (dom (order (S1,R))) +^ a ) ;
( ((order (S1,R)) ^ (order (S2,R))) . x = (order (S1,R)) . x & ((order (S1,R)) ^ (order (S2,R))) . y = (order (S2,R)) . a & x in Segm y ) by A25, A26, ORDINAL3:25, ORDINAL4:def 1;
then ( ((order (S1,R)) ^ (order (S2,R))) . x in S1 & ((order (S1,R)) ^ (order (S2,R))) . y in S2 & x < y ) by A1, A25, A26, FUNCT_1:def 3, NAT_1:44;
hence ( x <= y iff ((order (S1,R)) ^ (order (S2,R))) . x,((order (S1,R)) ^ (order (S2,R))) . y in R ) by A11; :: thesis: verum

end;

suppose A27: ( y in dom (order (S1,R)) & ex a being Ordinal st
( a in dom (order (S2,R)) & x = (dom (order (S1,R))) +^ a ) ) ; :: thesis: ( ( b₁ <= b₂ implies ((order (S1,R)) ^ (order (S2,R))) . b₁,((order (S1,R)) ^ (order (S2,R))) . b₂ in R ) & ( ((order (S1,R)) ^ (order (S2,R))) . b₁,((order (S1,R)) ^ (order (S2,R))) . b₂ in R implies b₁ <= b₂ ) )

then consider a being Ordinal such that
A28: ( a in dom (order (S2,R)) & x = (dom (order (S1,R))) +^ a ) ;
A29: ( ((order (S1,R)) ^ (order (S2,R))) . y = (order (S1,R)) . y & ((order (S1,R)) ^ (order (S2,R))) . x = (order (S2,R)) . a & y in Segm x ) by A27, A28, ORDINAL3:25, ORDINAL4:def 1;
then A30: ( ((order (S1,R)) ^ (order (S2,R))) . x in S2 & ((order (S1,R)) ^ (order (S2,R))) . y in S1 & y < x ) by A1, A27, A28, FUNCT_1:def 3, NAT_1:44;
thus ( x <= y implies ((order (S1,R)) ^ (order (S2,R))) . x,((order (S1,R)) ^ (order (S2,R))) . y in R ) by A29, NAT_1:44; :: thesis: ( ((order (S1,R)) ^ (order (S2,R))) . x,((order (S1,R)) ^ (order (S2,R))) . y in R implies x <= y )
assume A31: ((order (S1,R)) ^ (order (S2,R))) . x,((order (S1,R)) ^ (order (S2,R))) . y in R ; :: thesis: x <= y
((order (S1,R)) ^ (order (S2,R))) . y,((order (S1,R)) ^ (order (S2,R))) . x in R by A30, A11;
hence x <= y by A23, A13, A31, Def2; :: thesis: verum

end;

suppose A32: ( ex a being Ordinal st
( a in dom (order (S2,R)) & x = (dom (order (S1,R))) +^ a ) & ex a being Ordinal st
( a in dom (order (S2,R)) & y = (dom (order (S1,R))) +^ a ) ) ; :: thesis: ( b₁ <= b₂ iff ((order (S1,R)) ^ (order (S2,R))) . b₁,((order (S1,R)) ^ (order (S2,R))) . b₂ in R )

then consider a being Ordinal such that
A33: ( a in dom (order (S2,R)) & x = (dom (order (S1,R))) +^ a ) ;
consider b being Ordinal such that
A34: ( b in dom (order (S2,R)) & y = (dom (order (S1,R))) +^ b ) by A32;
reconsider a = a, b = b as Element of NAT by A33, A34;
( x <= y iff Segm x c= Segm y ) by NAT_1:39;
then ( x <= y iff Segm a c= Segm b ) by A33, A34, ORDINAL3:23, ORDINAL3:18;
then A35: ( x <= y iff a <= b ) by NAT_1:39;
( ((order (S1,R)) ^ (order (S2,R))) . x = (order (S2,R)) . a & ((order (S1,R)) ^ (order (S2,R))) . y = (order (S2,R)) . b ) by A33, A34, ORDINAL4:def 1;
hence ( x <= y iff ((order (S1,R)) ^ (order (S2,R))) . x,((order (S1,R)) ^ (order (S2,R))) . y in R ) by A33, A34, Def11, A35; :: thesis: verum

end;

end;

end;

hence order ((S1 \/ S2),R) = (order (S1,R)) ^ (order (S2,R)) by A12, A13, Def11; :: thesis: verum