let f be FinSequence of (TOP-REAL 2); 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; ( 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
; 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 16, 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 16, 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))))
XBOOLE_0:def 10 (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) c= L~ (f | (i + 1))proof
let x be
object ;
TARSKI:def 3 ( 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))
;
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;
suppose A22:
m < i
;
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;
verum end;
end;
let x be object ; TARSKI:def 3 ( not x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) or x in L~ (f | (i + 1)) )
assume A28:
x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1))))
; 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;
suppose
x in L~ (f | i)
;
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;
verum end;