let X, Y be set ; :: thesis:
assume that
a1: X is included_in_Seg and
a2: Y is included_in_Seg ; :: thesis:
consider i being Nat such that
A1: X c= Seg i by a1, FINSEQ_1:def 13;
consider j being Nat such that
A2: Y c= Seg j by a2, FINSEQ_1:def 13;
set r = Sgm (X \/ Y);
set q = Sgm Y;
set p = Sgm X;
Seg i, Seg j are_c=-comparable by Th19;
then ( Seg i c= Seg j or Seg j c= Seg i ) ;
then ( X c= Seg j or Y c= Seg i ) by A1, A2;
then A4: ( X \/ Y c= Seg i or X \/ Y c= Seg j ) by A1, A2, XBOOLE_1:8;
reconsider X1 = X, Y1 = Y as finite set by A1, A2;
bbb: X1 \/ Y1 is included_in_Seg by A4, FINSEQ_1:def 13;
thus ( ( for m, n being Nat st m in X & n in Y holds
m < n ) implies Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) ) :: thesis:

proof

defpred S₁[ Nat] means ( $1 in dom (Sgm X) implies (Sgm (X \/ Y)) . $1 = (Sgm X) . $1 );
assume A5: for m, n being Nat st m in X & n in Y holds
m < n ; :: thesis:
X /\ Y = {}

proof

set x = the Element of X /\ Y;
X = rng (Sgm X) by a1, FINSEQ_1:def 14;
then A6: X c= NAT ;
assume A7: not X /\ Y = {} ; :: thesis:
then the Element of X /\ Y in X by XBOOLE_0:def 4;
then reconsider m = the Element of X /\ Y as Element of NAT by A6;
A8: m in Y by A7, XBOOLE_0:def 4;
m in X by A7, XBOOLE_0:def 4;
hence contradiction by A5, A8; :: thesis:

end;

then A9: X misses Y ;
A10: len (Sgm (X \/ Y)) = card (X1 \/ Y1) by a1, a2, Th37
.= (card X1) + (card Y1) by A9, CARD_2:40
.= (len (Sgm X)) + (card Y1) by a1, Th37
.= (len (Sgm X)) + (len (Sgm Y)) by a2, Th37 ;

A11: now :: thesis:

let k be Nat; :: thesis:
assume A12: S₁[k] ; :: thesis:
thus S₁[k + 1] :: thesis:

proof

assume A13: k + 1 in dom (Sgm X) ; :: thesis:
then A14: (Sgm X) . (k + 1) in rng (Sgm X) by FUNCT_1:def 3;
then reconsider n = (Sgm X) . (k + 1) as Element of NAT ;
A15: n in X by a1, A14, FINSEQ_1:def 14;
len (Sgm X) <= len (Sgm (X \/ Y)) by A10, NAT_1:12;
then Seg (len (Sgm X)) c= Seg (len (Sgm (X \/ Y))) by FINSEQ_1:5;
then dom (Sgm X) c= Seg (len (Sgm (X \/ Y))) by FINSEQ_1:def 3;
then A16: dom (Sgm X) c= dom (Sgm (X \/ Y)) by FINSEQ_1:def 3;
then A17: (Sgm (X \/ Y)) . (k + 1) in rng (Sgm (X \/ Y)) by A13, FUNCT_1:def 3;
then reconsider m = (Sgm (X \/ Y)) . (k + 1) as Element of NAT ;
rng (Sgm (X \/ Y)) = X \/ Y by bbb, FINSEQ_1:def 14;
then A18: m in X \/ Y by A17;
assume A19: (Sgm (X \/ Y)) . (k + 1) <> (Sgm X) . (k + 1) ; :: thesis:
A20: k + 1 in dom (Sgm (X \/ Y)) by A13, A16;

now :: thesis:

per cases ;

suppose A21: k in dom (Sgm X) ; :: thesis:

then (Sgm X) . k in rng (Sgm X) by FUNCT_1:def 3;
then reconsider n1 = (Sgm X) . k as Element of NAT ;
(Sgm (X \/ Y)) . k in rng (Sgm (X \/ Y)) by A16, A21, FUNCT_1:def 3;
then reconsider m1 = (Sgm (X \/ Y)) . k as Element of NAT ;

now :: thesis:

per cases by A19, XXREAL_0:1;

suppose A22: m < n ; :: thesis:

A23: 1 <= k + 1 by A13, Th25;
not m in Y by A5, A15, A22;
then m in X by A18, XBOOLE_0:def 3;
then m in rng (Sgm X) by a1, FINSEQ_1:def 14;
then consider x being object such that
A24: x in dom (Sgm X) and
A25: (Sgm X) . x = m by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A24;
x <= len (Sgm X) by A24, Th25;
then A26: x < k + 1 by a1, A22, A25, A23, Th39;
k + 1 in Seg (len (Sgm (X \/ Y))) by A20, FINSEQ_1:def 3;
then A27: k + 1 <= len (Sgm (X \/ Y)) by FINSEQ_1:1;
k in Seg (len (Sgm X)) by A21, FINSEQ_1:def 3;
then A28: 1 <= k by FINSEQ_1:1;
k < k + 1 by XREAL_1:29;
then A29: n1 < m by bbb, A12, A21, A28, A27, FINSEQ_1:def 14;
A30: k <= len (Sgm X) by A21, Th25;
1 <= x by A24, Th25;
then k < x by a1, A25, A29, A30, Th39;
hence contradiction by A26, NAT_1:13; :: thesis:

end;

suppose A31: n < m ; :: thesis:

A32: 1 <= k + 1 by A13, Th25;
n in X \/ Y by A15, XBOOLE_0:def 3;
then n in rng (Sgm (X \/ Y)) by bbb, FINSEQ_1:def 14;
then consider x being object such that
A33: x in dom (Sgm (X \/ Y)) and
A34: (Sgm (X \/ Y)) . x = n by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A33;
x <= len (Sgm (X \/ Y)) by A33, Th25;
then A35: x < k + 1 by bbb, A31, A34, A32, Th39;
A36: k + 1 <= len (Sgm X) by A13, Th25;
A37: k < k + 1 by XREAL_1:29;
1 <= k by A21, Th25;
then A38: m1 < n by a1, A12, A21, A37, A36, FINSEQ_1:def 14;
A39: k <= len (Sgm (X \/ Y)) by A16, A21, Th25;
1 <= x by A33, Th25;
then k < x by bbb, A34, A38, A39, Th39;
hence contradiction by A35, NAT_1:13; :: thesis:

end;

hence contradiction ; :: thesis:

end;

suppose A40: not k in dom (Sgm X) ; :: thesis:

A41: k < k + 1 by XREAL_1:29;
( k < 1 or len (Sgm X) < k ) by A40, Th25;
then A42: ( k = 0 or ( len (Sgm X) < k + 1 & k + 1 <= len (Sgm X) ) ) by A13, A41, Th25, NAT_1:14, XXREAL_0:2;

now :: thesis:

per cases by A19, XXREAL_0:1;

suppose A43: m < n ; :: thesis:

then not m in Y by A5, A15;
then m in X by A18, XBOOLE_0:def 3;
then m in rng (Sgm X) by a1, FINSEQ_1:def 14;
then consider x being object such that
A44: x in dom (Sgm X) and
A45: (Sgm X) . x = m by FUNCT_1:def 3;
A46: 1 <= k + 1 by A13, Th25;
reconsider x = x as Element of NAT by A44;
x <= len (Sgm X) by A44, Th25;
then x < k + 1 by a1, A43, A45, A46, Th39;
hence contradiction by A42, A44, Th24, NAT_1:14; :: thesis:

end;

suppose A47: n < m ; :: thesis:

A48: 1 <= k + 1 by A13, Th25;
n in X \/ Y by A15, XBOOLE_0:def 3;
then n in rng (Sgm (X \/ Y)) by bbb, FINSEQ_1:def 14;
then consider x being object such that
A49: x in dom (Sgm (X \/ Y)) and
A50: (Sgm (X \/ Y)) . x = n by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A49;
x <= len (Sgm (X \/ Y)) by A49, Th25;
then x < k + 1 by bbb, A47, A50, A48, Th39;
hence contradiction by A42, A49, Th24, NAT_1:14; :: thesis:

end;

hence contradiction ; :: thesis:

end;

hence contradiction ; :: thesis:

end;

A51: S₁[ 0 ] by Th24;
A52: for k being Nat holds S₁[k] from NAT_1:sch 2(A51, A11);
defpred S₂[ Nat] means ( $1 in dom (Sgm Y) implies (Sgm (X \/ Y)) . ((len (Sgm X)) + $1) = (Sgm Y) . $1 );

A53: now :: thesis:

let k be Nat; :: thesis:
assume A54: S₂[k] ; :: thesis:
thus S₂[k + 1] :: thesis:

proof

set a = (len (Sgm X)) + (k + 1);
assume A55: k + 1 in dom (Sgm Y) ; :: thesis:
then k + 1 <= len (Sgm Y) by Th25;
then A56: (len (Sgm X)) + (k + 1) <= len (Sgm (X \/ Y)) by A10, XREAL_1:7;
A57: 1 <= k + 1 by NAT_1:12;
then 1 <= (len (Sgm X)) + (k + 1) by NAT_1:12;
then A58: (len (Sgm X)) + (k + 1) in dom (Sgm (X \/ Y)) by A56, Th25;
then A59: (Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1)) in rng (Sgm (X \/ Y)) by FUNCT_1:def 3;
reconsider m = (Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1)) as Element of NAT by A59;

A60: now :: thesis:

assume m in X ; :: thesis:
then m in rng (Sgm X) by a1, FINSEQ_1:def 14;
then consider x being object such that
A61: x in dom (Sgm X) and
A62: (Sgm X) . x = m by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A61;
x <= len (Sgm X) by A61, Th25;
then A63: x <= len (Sgm (X \/ Y)) by A10, NAT_1:12;
A64: Sgm (X \/ Y) is one-to-one by bbb;
1 <= x by A61, Th25;
then A65: x in dom (Sgm (X \/ Y)) by A63, Th25;
(Sgm (X \/ Y)) . x = (Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1)) by A52, A61, A62;
then x = (len (Sgm X)) + (k + 1) by A58, A64, A65;
then (len (Sgm X)) + (k + 1) <= (len (Sgm X)) + 0 by A61, Th25;
hence contradiction by XREAL_1:29; :: thesis:

end;

A66: (Sgm Y) . (k + 1) in rng (Sgm Y) by A55, FUNCT_1:def 3;
then reconsider n = (Sgm Y) . (k + 1) as Element of NAT ;
A67: n in Y by a2, A66, FINSEQ_1:def 14;
assume A68: (Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1)) <> (Sgm Y) . (k + 1) ; :: thesis:
A69: m in X \/ Y by bbb, A59, FINSEQ_1:def 14;

now :: thesis:

per cases ;

suppose A70: k in dom (Sgm Y) ; :: thesis:

then (Sgm Y) . k in rng (Sgm Y) by FUNCT_1:def 3;
then reconsider n1 = (Sgm Y) . k as Element of NAT ;
1 <= k by A70, Th25;
then A71: 1 <= (len (Sgm X)) + k by NAT_1:12;
A72: k <= len (Sgm Y) by A70, Th25;
then (len (Sgm X)) + k <= len (Sgm (X \/ Y)) by A10, XREAL_1:7;
then (len (Sgm X)) + k in dom (Sgm (X \/ Y)) by A71, Th25;
then (Sgm (X \/ Y)) . ((len (Sgm X)) + k) in rng (Sgm (X \/ Y)) by FUNCT_1:def 3;
then reconsider m1 = (Sgm (X \/ Y)) . ((len (Sgm X)) + k) as Element of NAT ;

now :: thesis:

per cases by A68, XXREAL_0:1;

suppose A73: m < n ; :: thesis:

A74: 1 <= k + 1 by A55, Th25;
m in Y by A69, A60, XBOOLE_0:def 3;
then m in rng (Sgm Y) by a2, FINSEQ_1:def 14;
then consider x being object such that
A75: x in dom (Sgm Y) and
A76: (Sgm Y) . x = m by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A75;
x <= len (Sgm Y) by A75, Th25;
then A77: x < k + 1 by a2, A73, A76, A74, Th39;
(len (Sgm X)) + k < ((len (Sgm X)) + k) + 1 by XREAL_1:29;
then A78: n1 < m by bbb, A54, A56, A70, A71, FINSEQ_1:def 14;
A79: k <= len (Sgm Y) by A70, Th25;
1 <= x by A75, Th25;
then k < x by a2, A76, A78, A79, Th39;
hence contradiction by A77, NAT_1:13; :: thesis:

end;

suppose A80: n < m ; :: thesis:

A81: 1 <= (len (Sgm X)) + (k + 1) by A57, NAT_1:12;
n in X \/ Y by A67, XBOOLE_0:def 3;
then n in rng (Sgm (X \/ Y)) by bbb, FINSEQ_1:def 14;
then consider x being object such that
A82: x in dom (Sgm (X \/ Y)) and
A83: (Sgm (X \/ Y)) . x = n by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A82;
x <= len (Sgm (X \/ Y)) by A82, Th25;
then A84: x < ((len (Sgm X)) + k) + 1 by a1, a2, A80, A83, A81, Th39;
A85: k + 1 <= len (Sgm Y) by A55, Th25;
A86: k < k + 1 by XREAL_1:29;
1 <= k by A70, Th25;
then A87: m1 < n by a2, A54, A70, A86, A85, FINSEQ_1:def 14;
A88: (len (Sgm X)) + k <= len (Sgm (X \/ Y)) by A10, A72, XREAL_1:7;
1 <= x by A82, Th25;
then (len (Sgm X)) + k < x by a1, a2, A83, A87, A88, Th39;
hence contradiction by A84, NAT_1:13; :: thesis:

end;

hence contradiction ; :: thesis:

end;

suppose A89: not k in dom (Sgm Y) ; :: thesis:

A90: k < k + 1 by XREAL_1:29;
( k < 1 or len (Sgm Y) < k ) by A89, Th25;
then A91: ( k = 0 or ( len (Sgm Y) < k + 1 & k + 1 <= len (Sgm Y) ) ) by A55, A90, Th25, NAT_1:14, XXREAL_0:2;

now :: thesis:

per cases by A68, XXREAL_0:1;

suppose A92: m < n ; :: thesis:

A93: 1 <= k + 1 by A55, Th25;
m in Y by A69, A60, XBOOLE_0:def 3;
then m in rng (Sgm Y) by a2, FINSEQ_1:def 14;
then consider x being object such that
A94: x in dom (Sgm Y) and
A95: (Sgm Y) . x = m by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A94;
x <= len (Sgm Y) by A94, Th25;
then x < k + 1 by a2, A92, A95, A93, Th39;
hence contradiction by A91, A94, Th24, NAT_1:14; :: thesis:

end;

suppose A96: n < m ; :: thesis:

A97: 1 <= (len (Sgm X)) + 1 by NAT_1:12;
n in X \/ Y by A67, XBOOLE_0:def 3;
then n in rng (Sgm (X \/ Y)) by bbb, FINSEQ_1:def 14;
then consider x being object such that
A98: x in dom (Sgm (X \/ Y)) and
A99: (Sgm (X \/ Y)) . x = n by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A98;
x <= len (Sgm (X \/ Y)) by A98, Th25;
then x < (len (Sgm X)) + 1 by a1, a2, A91, A96, A99, A97, Th39;
then A100: x <= len (Sgm X) by NAT_1:13;
1 <= x by A98, Th25;
then A101: x in dom (Sgm X) by A100, Th25;
then A102: (Sgm X) . x in rng (Sgm X) by FUNCT_1:def 3;
n = (Sgm X) . x by A52, A99, A101;
then n in X by a1, A102, FINSEQ_1:def 14;
hence contradiction by A5, A67; :: thesis:

end;

hence contradiction ; :: thesis:

end;

hence contradiction ; :: thesis:

end;

A103: S₂[ 0 ] by Th24;
for k being Nat holds S₂[k] from NAT_1:sch 2(A103, A53);
hence Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) by A10, A52, Th36; :: thesis:

end;

assume A104: Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) ; :: thesis:
let m, n be Nat; :: thesis:
assume that
A105: m in X and
A106: n in Y ; :: thesis:
n in rng (Sgm Y) by a2, A106, FINSEQ_1:def 14;
then consider y being object such that
A107: y in dom (Sgm Y) and
A108: (Sgm Y) . y = n by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A107;
A109: n = (Sgm (X \/ Y)) . ((len (Sgm X)) + y) by A104, A107, A108, FINSEQ_1:def 7;
y <= len (Sgm Y) by A107, Th25;
then (len (Sgm X)) + y <= (len (Sgm X)) + (len (Sgm Y)) by XREAL_1:7;
then A110: (len (Sgm X)) + y <= len (Sgm (X \/ Y)) by A104, FINSEQ_1:22;
m in rng (Sgm X) by a1, A105, FINSEQ_1:def 14;
then consider x being object such that
A111: x in dom (Sgm X) and
A112: (Sgm X) . x = m by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A111;
A113: x in Seg (len (Sgm X)) by A111, FINSEQ_1:def 3;
then A114: 1 <= x by FINSEQ_1:1;
A115: x <= len (Sgm X) by A113, FINSEQ_1:1;
y <> 0 by A107, Th24;
then A116: x < (len (Sgm X)) + y by A115, NAT_1:16, XXREAL_0:2;
m = (Sgm (X \/ Y)) . x by A104, A111, A112, FINSEQ_1:def 7;
hence m < n by bbb, A109, A114, A116, A110, FINSEQ_1:def 14; :: thesis: