let f be FinSequence of (); :: 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 ;
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 ; :: 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 ;
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 ;
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 ;
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 ;
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