let f be FinSequence of (TOP-REAL 2); :: thesis:
let i be Element of NAT ; :: thesis:
set M1 = { (LSeg ((f | (i + 1)),k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | (i + 1)) ) } ;
set Mi = { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } ;
assume that
A1: i in dom f and
A2: i + 1 in dom f ; :: thesis:
set p = f /. i;
set q = f /. (i + 1);
A3: i + 1 <= len f by A2, FINSEQ_3:25;
then Seg (i + 1) c= Seg (len f) by FINSEQ_1:5;
then Seg (i + 1) c= dom f by FINSEQ_1:def 3;
then Seg (i + 1) = (dom f) /\ (Seg (i + 1)) by XBOOLE_1:28;
then A4: ( f | (i + 1) = f | (Seg (i + 1)) & Seg (i + 1) = dom (f | (Seg (i + 1))) ) by FINSEQ_1:def 15, RELAT_1:61;
then A5: i + 1 = len (f | (i + 1)) by FINSEQ_1:def 3;
A6: 1 <= i by A1, FINSEQ_3:25;
then A7: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A3, TOPREAL1:def 3;
1 <= i + 1 by A2, FINSEQ_3:25;
then A8: i + 1 in dom (f | (i + 1)) by A5, FINSEQ_3:25;
A9: i <= i + 1 by NAT_1:11;
then i in dom (f | (i + 1)) by A6, A5, FINSEQ_3:25;
then A10: LSeg ((f | (i + 1)),i) = LSeg ((f /. i),(f /. (i + 1))) by A7, A8, Th24;
then A11: LSeg ((f /. i),(f /. (i + 1))) c= L~ (f | (i + 1)) by Th26;
i <= len f by A1, FINSEQ_3:25;
then Seg i c= Seg (len f) by FINSEQ_1:5;
then Seg i c= dom f by FINSEQ_1:def 3;
then (dom f) /\ (Seg i) = Seg i by XBOOLE_1:28;
then A12: ( f | i = f | (Seg i) & dom (f | (Seg i)) = Seg i ) by FINSEQ_1:def 15, RELAT_1:61;
then A13: i = len (f | i) by FINSEQ_1:def 3;
A14: Seg (len (f | (i + 1))) = dom (f | (i + 1)) by FINSEQ_1:def 3;
thus L~ (f | (i + 1)) c= (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in L~ (f | (i + 1)) ; :: thesis:
then consider X being set such that
A15: x in X and
A16: X in { (LSeg ((f | (i + 1)),k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | (i + 1)) ) } by TARSKI:def 4;
consider m being Element of NAT such that
A17: X = LSeg ((f | (i + 1)),m) and
A18: 1 <= m and
A19: m + 1 <= len (f | (i + 1)) by A16;
A20: m <= i by A5, A19, XREAL_1:6;

per cases by A20, XXREAL_0:1;

suppose m = i ; :: thesis:

then X c= (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) by A10, A17, XBOOLE_1:7;
hence x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) by A15; :: thesis:

end;

suppose A21: m < i ; :: thesis:

then m <= i + 1 by NAT_1:13;
then A22: m in dom (f | (i + 1)) by A4, A18, FINSEQ_1:1;
A23: m in dom (f | i) by A12, A18, A21, FINSEQ_1:1;
A24: 1 <= m + 1 by A18, NAT_1:13;
A25: m + 1 <= i by A21, NAT_1:13;
then A26: m + 1 in dom (f | i) by A12, A24, FINSEQ_1:1;
m + 1 in dom (f | (i + 1)) by A14, A19, A24, FINSEQ_1:1;
then X = LSeg (f,m) by A17, A22, Th24
.= LSeg ((f | i),m) by A23, A26, Th24 ;
then X in { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } by A13, A18, A25;
then x in union { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } by A15, TARSKI:def 4;
hence x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) by XBOOLE_0:def 3; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A27: x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) ; :: thesis:

per cases by A27, XBOOLE_0:def 3;

suppose x in L~ (f | i) ; :: thesis:

then consider X being set such that
A28: x in X and
A29: X in { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } by TARSKI:def 4;
consider m being Element of NAT such that
A30: X = LSeg ((f | i),m) and
A31: 1 <= m and
A32: m + 1 <= len (f | i) by A29;
A33: 1 <= m + 1 by NAT_1:11;
then A34: m + 1 in dom (f | i) by A32, FINSEQ_3:25;
m <= m + 1 by NAT_1:11;
then A35: m <= len (f | i) by A32, XXREAL_0:2;
then m <= len (f | (i + 1)) by A5, A13, A9, XXREAL_0:2;
then A36: m in dom (f | (i + 1)) by A31, FINSEQ_3:25;
A37: m + 1 <= len (f | (i + 1)) by A5, A13, A9, A32, XXREAL_0:2;
then A38: m + 1 in dom (f | (i + 1)) by A33, FINSEQ_3:25;
m in dom (f | i) by A31, A35, FINSEQ_3:25;
then X = LSeg (f,m) by A30, A34, Th24
.= LSeg ((f | (i + 1)),m) by A36, A38, Th24 ;
then X in { (LSeg ((f | (i + 1)),k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | (i + 1)) ) } by A31, A37;
hence x in L~ (f | (i + 1)) by A28, TARSKI:def 4; :: thesis:

end;

suppose x in LSeg ((f /. i),(f /. (i + 1))) ; :: thesis:

hence x in L~ (f | (i + 1)) by A11; :: thesis:

end;