let f be FinSequence of (TOP-REAL 2); :: thesis: for i being Nat st f is s.n.c. holds
f | i is s.n.c.
let i be 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 7 :: 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;
then A2: (LSeg (f,n)) /\ (LSeg (f,m)) = {} ;

now :: thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)

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

now :: thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)

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

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

now :: thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)

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 A6: LSeg (f,n) = LSeg ((f | i),n) by A5, TOPREAL3:17;

now :: thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)

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

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

now :: thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),m)) = {}

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 A2, A6, A7, TOPREAL3:17; :: 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:25;
then LSeg ((f | i),m) = {} by NAT_1:11, TOPREAL1:def 3;
hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),m)) = {} ; :: thesis: verum

end;

end;

end;

hence LSeg ((f | i),n) misses LSeg ((f | i),m) ; :: 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:25;
then ( not 1 <= m or not m + 1 <= len (f | i) ) by A3, XXREAL_0:2;
then LSeg ((f | i),m) = {} by TOPREAL1:def 3;
hence LSeg ((f | i),n) misses LSeg ((f | i),m) ; :: 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:25;
then LSeg ((f | i),n) = {} by NAT_1:11, TOPREAL1:def 3;
hence LSeg ((f | i),n) misses LSeg ((f | i),m) ; :: 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:25;
then ( not 1 <= n or not n + 1 <= len (f | i) ) by A4, XXREAL_0:2;
then LSeg ((f | i),n) = {} by TOPREAL1:def 3;
hence LSeg ((f | i),n) misses LSeg ((f | i),m) ; :: 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