let f be s.c.c. FinSequence of (TOP-REAL 2); :: thesis: for n being Nat st 1 <= n holds
f /^ n is s.n.c.
let n be 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 7 :: 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 i < 1 ; :: thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j)

then LSeg ((f /^ n),i) = {} by TOPREAL1:def 3;
then (LSeg ((f /^ n),i)) /\ (LSeg ((f /^ n),j)) = {} ;
hence LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) by XBOOLE_0:def 7; :: thesis: verum

end;

suppose n > len f ; :: thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j)

then f /^ n = <*> the carrier of (TOP-REAL 2) by RFINSEQ:def 1;
then ( not 1 <= i or not i + 1 <= len (f /^ n) ) ;
then LSeg ((f /^ n),i) = {} by TOPREAL1:def 3;
then (LSeg ((f /^ n),i)) /\ (LSeg ((f /^ n),j)) = {} ;
hence LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) by XBOOLE_0:def 7; :: thesis: verum

end;

suppose len (f /^ n) <= j ; :: thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j)

then len (f /^ n) < j + 1 by NAT_1:13;
then LSeg ((f /^ n),j) = {} by TOPREAL1:def 3;
then (LSeg ((f /^ n),i)) /\ (LSeg ((f /^ n),j)) = {} ;
hence LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) by XBOOLE_0:def 7; :: thesis: verum

end;

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)

A6: j < (len f) - n by A3, A5, RFINSEQ:def 1;
then A7: j + 1 <= (len f) - n by INT_1:7;
1 + 1 <= i + 1 by A4, XREAL_1:6;
then 1 + 1 <= j by A2, XXREAL_0:2;
then 1 < j by NAT_1:13;
then A8: LSeg (f,(j + n)) = LSeg ((f /^ n),j) by A7, SPPOL_2:5;
(i + 1) + n < j + n by A2, XREAL_1:6;
then A9: (i + n) + 1 < j + n ;
j <= j + 1 by NAT_1:11;
then i + 1 <= j + 1 by A2, XXREAL_0:2;
then A10: i + 1 <= (len f) - n by A7, XXREAL_0:2;
1 + 1 <= i + n by A1, A4, XREAL_1:7;
then A11: 1 < i + n by NAT_1:13;
j + n < len f by A6, XREAL_1:20;
then LSeg (f,(i + n)) misses LSeg (f,(j + n)) by A11, A9, GOBOARD5:def 4;
hence LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) by A4, A8, A10, SPPOL_2:5; :: thesis: verum

end;

end;