let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st f is s.n.c. holds

f -: p is s.n.c.

let p be Point of (TOP-REAL 2); :: 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

f -: p is s.n.c.

let p be Point of (TOP-REAL 2); :: 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