let f be FinSequence of (TOP-REAL 2); :: thesis: for i being Element of NAT st f is s.n.c. holds
f | i is s.n.c.
let i be Element of NAT ; :: thesis: ( f is s.n.c. implies f | i is s.n.c. )
assume A1: f is s.n.c. ; :: thesis: f | i is s.n.c.
set f1 = f | i;
let n, m be Nat; :: according to TOPREAL1:def 9 :: thesis: ( m <= n + 1 or LSeg ((f | i),n) misses LSeg ((f | i),m) )
assume m > n + 1 ; :: thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)
then LSeg (f,n) misses LSeg (f,m) by A1, TOPREAL1:def 9;
then A3: (LSeg (f,n)) /\ (LSeg (f,m)) = {} by XBOOLE_0:def 7;

now

A4: m <= m + 1 by NAT_1:11;
A5: n <= n + 1 by NAT_1:11;

now

per cases ( n in dom (f | i) or not n in dom (f | i) ) ;

suppose A6: n in dom (f | i) ; :: thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)

now

per cases ( n + 1 in dom (f | i) or not n + 1 in dom (f | i) ) ;

suppose n + 1 in dom (f | i) ; :: thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)

then A7: LSeg (f,n) = LSeg ((f | i),n) by A6, TOPREAL3:24;

now

per cases ( m in dom (f | i) or not m in dom (f | i) ) ;

suppose A8: m in dom (f | i) ; :: thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)

now

per cases ( m + 1 in dom (f | i) or not m + 1 in dom (f | i) ) ;

suppose m + 1 in dom (f | i) ; :: thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),m)) = {}

hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),m)) = {} by A3, A7, A8, TOPREAL3:24; :: thesis: verum

end;

suppose not m + 1 in dom (f | i) ; :: thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),m)) = {}

then ( not 1 <= m + 1 or not m + 1 <= len (f | i) ) by FINSEQ_3:27;
then LSeg ((f | i),m) = {} by NAT_1:11, TOPREAL1:def 5;
hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),m)) = {} ; :: thesis: verum

end;

end;

end;

hence LSeg ((f | i),n) misses LSeg ((f | i),m) by XBOOLE_0:def 7; :: thesis: verum

end;

suppose not m in dom (f | i) ; :: thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)

then ( not 1 <= m or not m <= len (f | i) ) by FINSEQ_3:27;
then ( not 1 <= m or not m + 1 <= len (f | i) ) by A4, XXREAL_0:2;
then LSeg ((f | i),m) = {} by TOPREAL1:def 5;
hence LSeg ((f | i),n) misses LSeg ((f | i),m) by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

hence LSeg ((f | i),n) misses LSeg ((f | i),m) ; :: thesis: verum

end;

suppose not n + 1 in dom (f | i) ; :: thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)

then ( not 1 <= n + 1 or not n + 1 <= len (f | i) ) by FINSEQ_3:27;
then LSeg ((f | i),n) = {} by NAT_1:11, TOPREAL1:def 5;
hence LSeg ((f | i),n) misses LSeg ((f | i),m) by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

hence LSeg ((f | i),n) misses LSeg ((f | i),m) ; :: thesis: verum

end;

suppose not n in dom (f | i) ; :: thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)

then ( not 1 <= n or not n <= len (f | i) ) by FINSEQ_3:27;
then ( not 1 <= n or not n + 1 <= len (f | i) ) by A5, XXREAL_0:2;
then LSeg ((f | i),n) = {} by TOPREAL1:def 5;
hence LSeg ((f | i),n) misses LSeg ((f | i),m) by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

hence LSeg ((f | i),n) misses LSeg ((f | i),m) ; :: thesis: verum

end;

hence LSeg ((f | i),n) misses LSeg ((f | i),m) ; :: thesis: verum