let f be s.c.c. FinSequence of (TOP-REAL 2); :: thesis: for n being Element of NAT st 1 <= n holds
f /^ n is s.n.c.
let n be Element of NAT ; :: thesis: ( 1 <= n implies f /^ n is s.n.c. )
assume A1:
1 <= n
; :: thesis: f /^ n is s.n.c.
let i, j be Nat; :: according to TOPREAL1:def 9 :: thesis: ( j <= i + 1 or LSeg (f /^ n),i misses LSeg (f /^ n),j )
assume A2:
i + 1 < j
; :: thesis: LSeg (f /^ n),i misses LSeg (f /^ n),j
per cases
( i < 1 or n > len f or len (f /^ n) <= j or ( n <= len f & 1 <= i & j < len (f /^ n) ) )
;
suppose that A3:
n <= len f
and A4:
1
<= i
and A5:
j < len (f /^ n)
;
:: thesis: LSeg (f /^ n),i misses LSeg (f /^ n),j
1
+ 1
<= i + 1
by A4, XREAL_1:8;
then
1
+ 1
<= j
by A2, XXREAL_0:2;
then A6:
1
< j
by NAT_1:13;
1
+ 1
<= i + n
by A1, A4, XREAL_1:9;
then A7:
1
< i + n
by NAT_1:13;
A8:
j < (len f) - n
by A3, A5, RFINSEQ:def 2;
then A9:
j + n < len f
by XREAL_1:22;
(i + 1) + n < j + n
by A2, XREAL_1:8;
then
(i + n) + 1
< j + n
;
then A10:
LSeg f,
(i + n) misses LSeg f,
(j + n)
by A7, A9, GOBOARD5:def 4;
A11:
j + 1
<= (len f) - n
by A8, INT_1:20;
then A12:
LSeg f,
(j + n) = LSeg (f /^ n),
j
by A6, SPPOL_2:5;
j <= j + 1
by NAT_1:11;
then
i + 1
<= j + 1
by A2, XXREAL_0:2;
then
i + 1
<= (len f) - n
by A11, XXREAL_0:2;
hence
LSeg (f /^ n),
i misses LSeg (f /^ n),
j
by A4, A10, A12, SPPOL_2:5;
:: thesis: verum