let f be FinSequence of ; :: thesis: for p being Point of st f is s.n.c. holds
f -: p is s.n.c.
let p be Point of ; :: thesis: ( f is s.n.c. implies f -: p is s.n.c. )
f -: p = f | (p .. f) by FINSEQ_5:def 1;
hence ( f is s.n.c. implies f -: p is s.n.c. ) ; :: thesis: verum