let f be FinSequence of ; :: 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;
A2: ( dom f = Seg (len f) & f | i = f | (Seg i) ) by FINSEQ_1:def 3, FINSEQ_1:def 15;
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