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

f :- p is s.n.c.

let p be Point of (TOP-REAL 2); :: thesis: ( p in rng f & f is s.n.c. implies f :- p is s.n.c. )

assume p in rng f ; :: thesis: ( not f is s.n.c. or f :- p is s.n.c. )

then ex i being Element of NAT st

( i + 1 = p .. f & f :- p = f /^ i ) by FINSEQ_5:49;

hence ( not f is s.n.c. or f :- p is s.n.c. ) ; :: thesis: verum

f :- p is s.n.c.

let p be Point of (TOP-REAL 2); :: thesis: ( p in rng f & f is s.n.c. implies f :- p is s.n.c. )

assume p in rng f ; :: thesis: ( not f is s.n.c. or f :- p is s.n.c. )

then ex i being Element of NAT st

( i + 1 = p .. f & f :- p = f /^ i ) by FINSEQ_5:49;

hence ( not f is s.n.c. or f :- p is s.n.c. ) ; :: thesis: verum