let l3 be Element of NAT ; :: thesis: for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for l1, l2 being Nat st l1 <= l2,S & l2 <= l3,S holds
l1 <= l3,S
let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for l1, l2 being Nat st l1 <= l2,S & l2 <= l3,S holds
l1 <= l3,S
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: for l1, l2 being Nat st l1 <= l2,S & l2 <= l3,S holds
l1 <= l3,S
let l1, l2 be Nat; :: thesis: ( l1 <= l2,S & l2 <= l3,S implies l1 <= l3,S )
given f1 being non empty FinSequence of NAT such that A1: f1 /. 1 = l1 and
A2: f1 /. (len f1) = l2 and
A3: for n being Element of NAT st 1 <= n & n < len f1 holds
f1 /. (n + 1) in SUCC ((f1 /. n),S) ; :: according to AMI_WSTD:def 1 :: thesis: ( not l2 <= l3,S or l1 <= l3,S )
given f2 being non empty FinSequence of NAT such that A4: f2 /. 1 = l2 and
A5: f2 /. (len f2) = l3 and
A6: for n being Element of NAT st 1 <= n & n < len f2 holds
f2 /. (n + 1) in SUCC ((f2 /. n),S) ; :: according to AMI_WSTD:def 1 :: thesis: l1 <= l3,S
take f1 ^' f2 ; :: according to AMI_WSTD:def 1 :: thesis: ( (f1 ^' f2) /. 1 = l1 & (f1 ^' f2) /. (len (f1 ^' f2)) = l3 & ( for n being Element of NAT st 1 <= n & n < len (f1 ^' f2) holds
(f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S) ) )
thus (f1 ^' f2) /. 1 = l1 by A1, FINSEQ_6:155; :: thesis: ( (f1 ^' f2) /. (len (f1 ^' f2)) = l3 & ( for n being Element of NAT st 1 <= n & n < len (f1 ^' f2) holds
(f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S) ) )

now :: thesis: (f1 ^' f2) /. (len (f1 ^' f2)) = l3

per cases ( f2 is trivial or not f2 is trivial ) ;

suppose f2 is trivial ; :: thesis: (f1 ^' f2) /. (len (f1 ^' f2)) = l3

then A7: ex x being Element of NAT st f2 = <*x*> by FINSEQ_6:107;
then f1 ^' f2 = f1 by FINSEQ_6:158;
hence (f1 ^' f2) /. (len (f1 ^' f2)) = l3 by A2, A4, A5, A7, FINSEQ_1:39; :: thesis: verum

end;

suppose not f2 is trivial ; :: thesis: (f1 ^' f2) /. (len (f1 ^' f2)) = l3

hence (f1 ^' f2) /. (len (f1 ^' f2)) = l3 by A5, FINSEQ_6:156; :: thesis: verum

end;

end;

end;

hence (f1 ^' f2) /. (len (f1 ^' f2)) = l3 ; :: thesis: for n being Element of NAT st 1 <= n & n < len (f1 ^' f2) holds
(f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S)
let n be Element of NAT ; :: thesis: ( 1 <= n & n < len (f1 ^' f2) implies (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S) )
assume that
A8: 1 <= n and
A9: n < len (f1 ^' f2) ; :: thesis: (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S)
A10: (len (f1 ^' f2)) + 1 = (len f1) + (len f2) by FINSEQ_6:139;

per cases ( n < len f1 or n = len f1 or n > len f1 ) by XXREAL_0:1;

suppose A11: n < len f1 ; :: thesis: (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S)

then n + 1 <= len f1 by NAT_1:13;
then A12: (f1 ^' f2) /. (n + 1) = f1 /. (n + 1) by FINSEQ_6:159, NAT_1:11;
(f1 ^' f2) /. n = f1 /. n by A8, A11, FINSEQ_6:159;
hence (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S) by A3, A8, A11, A12; :: thesis: verum

end;

suppose A13: n = len f1 ; :: thesis: (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S)

then A14: (f1 ^' f2) /. n = f2 /. 1 by A2, A4, A8, FINSEQ_6:159;
n + 1 < (len (f1 ^' f2)) + 1 by A9, XREAL_1:6;
then A15: 1 < len f2 by A10, A13, XREAL_1:6;
then (f1 ^' f2) /. (n + 1) = f2 /. (1 + 1) by A13, FINSEQ_6:160;
hence (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S) by A6, A14, A15; :: thesis: verum

end;

suppose A16: n > len f1 ; :: thesis: (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S)

then consider m being Nat such that
A17: (len f1) + m = n by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
A18: (len f1) + m > (len f1) + 0 by A16, A17;
((len f1) + m) + 1 < (len f1) + (len f2) by A9, A10, A17, XREAL_1:6;
then (len f1) + (m + 1) < (len f1) + (len f2) ;
then A19: m + 1 < len f2 by XREAL_1:6;
A20: (f1 ^' f2) /. (n + 1) = (f1 ^' f2) /. ((len f1) + (m + 1)) by A17
.= f2 /. ((m + 1) + 1) by A19, FINSEQ_6:160, NAT_1:11 ;
m <= m + 1 by NAT_1:11;
then m < len f2 by A19, XXREAL_0:2;
then (f1 ^' f2) /. n = f2 /. (m + 1) by A17, A18, FINSEQ_6:160, NAT_1:14;
hence (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S) by A6, A19, A20, NAT_1:11; :: thesis: verum

end;

end;