let f be FinSequence of (TOP-REAL 2); :: thesis: for i being Element of 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 Element of 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 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 A1:
( i in dom f & 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);
A2:
( Seg (len (f | (i + 1))) = dom (f | (i + 1)) & Seg (len f) = dom f & f | (i + 1) = f | (Seg (i + 1)) & f | i = f | (Seg i) )
by FINSEQ_1:def 3, FINSEQ_1:def 15;
A3:
( 1 <= i + 1 & i + 1 <= len f & 1 <= i & i <= len f )
by A1, FINSEQ_3:27;
then
( Seg (i + 1) c= Seg (len f) & Seg i c= Seg (len f) )
by FINSEQ_1:7;
then
( Seg (i + 1) c= dom f & Seg i c= dom f )
by FINSEQ_1:def 3;
then
( Seg (i + 1) = (dom f) /\ (Seg (i + 1)) & (dom f) /\ (Seg i) = Seg i )
by XBOOLE_1:28;
then A4:
( Seg (i + 1) = dom (f | (Seg (i + 1))) & dom (f | (Seg i)) = Seg i )
by RELAT_1:90;
then A5:
( i + 1 = len (f | (i + 1)) & i = len (f | i) & i <= i + 1 )
by A2, FINSEQ_1:def 3, NAT_1:11;
then
( LSeg f,i = LSeg (f /. i),(f /. (i + 1)) & i + 1 in dom (f | (i + 1)) & i in dom (f | (i + 1)) )
by A3, FINSEQ_3:27, TOPREAL1:def 5;
then A6:
LSeg (f | (i + 1)),i = LSeg (f /. i),(f /. (i + 1))
by A1, Th24;
then A7:
LSeg (f /. i),(f /. (i + 1)) c= L~ (f | (i + 1))
by Th26;
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
set ;
:: 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 A8:
(
x in X &
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 A9:
(
X = LSeg (f | (i + 1)),
m & 1
<= m &
m + 1
<= len (f | (i + 1)) )
by A8;
A10:
m <= i
by A5, A9, XREAL_1:8;
per cases
( m = i or m < i )
by A10, XXREAL_0:1;
suppose A11:
m < i
;
:: thesis: x in (L~ (f | i)) \/ (LSeg (f /. i),(f /. (i + 1)))then A12:
(
m <= i &
m + 1
<= i &
m <= m + 1 &
i <= i + 1 )
by NAT_1:13;
A13:
(
m + 1
<= len (f | i) & 1
<= m + 1 )
by A5, A9, A11, NAT_1:13;
then A14:
(
m in dom (f | i) &
m + 1
in dom (f | i) &
m <= i + 1 )
by A2, A4, A9, A12, FINSEQ_1:3, XXREAL_0:2;
then
(
m in dom (f | (i + 1)) &
m + 1
in dom (f | (i + 1)) )
by A2, A4, A9, A13, FINSEQ_1:3;
then X =
LSeg f,
m
by A1, A9, Th24
.=
LSeg (f | i),
m
by A1, A14, Th24
;
then
X in { (LSeg (f | i),n) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) }
by A5, A9, A12;
then
x in union { (LSeg (f | i),n) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) }
by A8, TARSKI:def 4;
hence
x in (L~ (f | i)) \/ (LSeg (f /. i),(f /. (i + 1)))
by XBOOLE_0:def 3;
:: thesis: verum end;
end;
let x be set ; :: 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)) )
assume A15:
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 A15, XBOOLE_0:def 3;
suppose
x in L~ (f | i)
;
:: thesis: x in L~ (f | (i + 1))then consider X being
set such that A16:
(
x in X &
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 A17:
(
X = LSeg (f | i),
m & 1
<= m &
m + 1
<= len (f | i) )
by A16;
m <= m + 1
by NAT_1:11;
then A18:
( 1
<= m &
m <= len (f | i) & 1
<= m + 1 &
m + 1
<= len (f | i) )
by A17, XXREAL_0:2;
then A19:
(
m in dom (f | i) &
m + 1
in dom (f | i) &
m <= len (f | (i + 1)) &
m + 1
<= len (f | (i + 1)) )
by A5, FINSEQ_3:27, XXREAL_0:2;
then A20:
(
m in dom (f | (i + 1)) &
m + 1
in dom (f | (i + 1)) &
len (f | i) <= len (f | (i + 1)) )
by A5, A18, FINSEQ_3:27;
X =
LSeg f,
m
by A1, A17, A19, Th24
.=
LSeg (f | (i + 1)),
m
by A1, A20, Th24
;
then
X in { (LSeg (f | (i + 1)),k) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | (i + 1)) ) }
by A17, A19;
hence
x in L~ (f | (i + 1))
by A16, TARSKI:def 4;
:: thesis: verum end;