let f be FinSequence of (TOP-REAL 2); :: thesis: for i being Nat st i in dom f & i + 1 in dom f holds

L~ (f | (i + 1)) = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1))))

let i be Nat; :: thesis: ( i in dom f & i + 1 in dom f implies L~ (f | (i + 1)) = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) )

set M1 = { (LSeg ((f | (i + 1)),k)) where k is Nat : ( 1 <= k & k + 1 <= len (f | (i + 1)) ) } ;

set Mi = { (LSeg ((f | i),n)) where n is Nat : ( 1 <= n & n + 1 <= len (f | i) ) } ;

assume that

A1: i in dom f and

A2: i + 1 in dom f ; :: thesis: L~ (f | (i + 1)) = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1))))

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, Th17;

then A11: LSeg ((f /. i),(f /. (i + 1))) c= L~ (f | (i + 1)) by Th19;

A12: i in NAT by ORDINAL1:def 12;

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 A13: ( f | i = f | (Seg i) & dom (f | (Seg i)) = Seg i ) by FINSEQ_1:def 15, RELAT_1:61;

then A14: i = len (f | i) by A12, FINSEQ_1:def 3;

A15: 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: (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) c= L~ (f | (i + 1))

assume A28: x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) ; :: thesis: x in L~ (f | (i + 1))

L~ (f | (i + 1)) = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1))))

let i be Nat; :: thesis: ( i in dom f & i + 1 in dom f implies L~ (f | (i + 1)) = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) )

set M1 = { (LSeg ((f | (i + 1)),k)) where k is Nat : ( 1 <= k & k + 1 <= len (f | (i + 1)) ) } ;

set Mi = { (LSeg ((f | i),n)) where n is Nat : ( 1 <= n & n + 1 <= len (f | i) ) } ;

assume that

A1: i in dom f and

A2: i + 1 in dom f ; :: thesis: L~ (f | (i + 1)) = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1))))

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, Th17;

then A11: LSeg ((f /. i),(f /. (i + 1))) c= L~ (f | (i + 1)) by Th19;

A12: i in NAT by ORDINAL1:def 12;

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 A13: ( f | i = f | (Seg i) & dom (f | (Seg i)) = Seg i ) by FINSEQ_1:def 15, RELAT_1:61;

then A14: i = len (f | i) by A12, FINSEQ_1:def 3;

A15: 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: (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) c= L~ (f | (i + 1))

proof

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

assume x in L~ (f | (i + 1)) ; :: thesis: x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1))))

then consider X being set such that

A16: x in X and

A17: X in { (LSeg ((f | (i + 1)),k)) where k is Nat : ( 1 <= k & k + 1 <= len (f | (i + 1)) ) } by TARSKI:def 4;

consider m being Nat such that

A18: X = LSeg ((f | (i + 1)),m) and

A19: 1 <= m and

A20: m + 1 <= len (f | (i + 1)) by A17;

A21: m <= i by A5, A20, XREAL_1:6;

end;assume x in L~ (f | (i + 1)) ; :: thesis: x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1))))

then consider X being set such that

A16: x in X and

A17: X in { (LSeg ((f | (i + 1)),k)) where k is Nat : ( 1 <= k & k + 1 <= len (f | (i + 1)) ) } by TARSKI:def 4;

consider m being Nat such that

A18: X = LSeg ((f | (i + 1)),m) and

A19: 1 <= m and

A20: m + 1 <= len (f | (i + 1)) by A17;

A21: m <= i by A5, A20, XREAL_1:6;

per cases
( m = i or m < i )
by A21, XXREAL_0:1;

end;

suppose
m = i
; :: thesis: x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1))))

then
X c= (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1))))
by A10, A18, XBOOLE_1:7;

hence x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) by A16; :: thesis: verum

end;hence x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) by A16; :: thesis: verum

suppose A22:
m < i
; :: thesis: x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1))))

then
m <= i + 1
by NAT_1:13;

then A23: m in dom (f | (i + 1)) by A4, A19, FINSEQ_1:1;

A24: m in dom (f | i) by A13, A19, A22, FINSEQ_1:1;

A25: 1 <= m + 1 by A19, NAT_1:13;

A26: m + 1 <= i by A22, NAT_1:13;

then A27: m + 1 in dom (f | i) by A13, A25, FINSEQ_1:1;

m + 1 in dom (f | (i + 1)) by A15, A20, A25, FINSEQ_1:1;

then X = LSeg (f,m) by A18, A23, Th17

.= LSeg ((f | i),m) by A24, A27, Th17 ;

then X in { (LSeg ((f | i),n)) where n is Nat : ( 1 <= n & n + 1 <= len (f | i) ) } by A14, A19, A26;

then x in union { (LSeg ((f | i),n)) where n is Nat : ( 1 <= n & n + 1 <= len (f | i) ) } by A16, TARSKI:def 4;

hence x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) by XBOOLE_0:def 3; :: thesis: verum

end;then A23: m in dom (f | (i + 1)) by A4, A19, FINSEQ_1:1;

A24: m in dom (f | i) by A13, A19, A22, FINSEQ_1:1;

A25: 1 <= m + 1 by A19, NAT_1:13;

A26: m + 1 <= i by A22, NAT_1:13;

then A27: m + 1 in dom (f | i) by A13, A25, FINSEQ_1:1;

m + 1 in dom (f | (i + 1)) by A15, A20, A25, FINSEQ_1:1;

then X = LSeg (f,m) by A18, A23, Th17

.= LSeg ((f | i),m) by A24, A27, Th17 ;

then X in { (LSeg ((f | i),n)) where n is Nat : ( 1 <= n & n + 1 <= len (f | i) ) } by A14, A19, A26;

then x in union { (LSeg ((f | i),n)) where n is Nat : ( 1 <= n & n + 1 <= len (f | i) ) } by A16, TARSKI:def 4;

hence x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) by XBOOLE_0:def 3; :: thesis: verum

assume A28: x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) ; :: thesis: x in L~ (f | (i + 1))

per cases
( x in L~ (f | i) or x in LSeg ((f /. i),(f /. (i + 1))) )
by A28, XBOOLE_0:def 3;

end;

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

then consider X being set such that

A29: x in X and

A30: X in { (LSeg ((f | i),n)) where n is Nat : ( 1 <= n & n + 1 <= len (f | i) ) } by TARSKI:def 4;

consider m being Nat such that

A31: X = LSeg ((f | i),m) and

A32: 1 <= m and

A33: m + 1 <= len (f | i) by A30;

A34: 1 <= m + 1 by NAT_1:11;

then A35: m + 1 in dom (f | i) by A33, FINSEQ_3:25;

m <= m + 1 by NAT_1:11;

then A36: m <= len (f | i) by A33, XXREAL_0:2;

then m <= len (f | (i + 1)) by A5, A14, A9, XXREAL_0:2;

then A37: m in dom (f | (i + 1)) by A32, FINSEQ_3:25;

A38: m + 1 <= len (f | (i + 1)) by A5, A14, A9, A33, XXREAL_0:2;

then A39: m + 1 in dom (f | (i + 1)) by A34, FINSEQ_3:25;

m in dom (f | i) by A32, A36, FINSEQ_3:25;

then X = LSeg (f,m) by A31, A35, Th17

.= LSeg ((f | (i + 1)),m) by A37, A39, Th17 ;

then X in { (LSeg ((f | (i + 1)),k)) where k is Nat : ( 1 <= k & k + 1 <= len (f | (i + 1)) ) } by A32, A38;

hence x in L~ (f | (i + 1)) by A29, TARSKI:def 4; :: thesis: verum

end;A29: x in X and

A30: X in { (LSeg ((f | i),n)) where n is Nat : ( 1 <= n & n + 1 <= len (f | i) ) } by TARSKI:def 4;

consider m being Nat such that

A31: X = LSeg ((f | i),m) and

A32: 1 <= m and

A33: m + 1 <= len (f | i) by A30;

A34: 1 <= m + 1 by NAT_1:11;

then A35: m + 1 in dom (f | i) by A33, FINSEQ_3:25;

m <= m + 1 by NAT_1:11;

then A36: m <= len (f | i) by A33, XXREAL_0:2;

then m <= len (f | (i + 1)) by A5, A14, A9, XXREAL_0:2;

then A37: m in dom (f | (i + 1)) by A32, FINSEQ_3:25;

A38: m + 1 <= len (f | (i + 1)) by A5, A14, A9, A33, XXREAL_0:2;

then A39: m + 1 in dom (f | (i + 1)) by A34, FINSEQ_3:25;

m in dom (f | i) by A32, A36, FINSEQ_3:25;

then X = LSeg (f,m) by A31, A35, Th17

.= LSeg ((f | (i + 1)),m) by A37, A39, Th17 ;

then X in { (LSeg ((f | (i + 1)),k)) where k is Nat : ( 1 <= k & k + 1 <= len (f | (i + 1)) ) } by A32, A38;

hence x in L~ (f | (i + 1)) by A29, TARSKI:def 4; :: thesis: verum