let p be Point of (TOP-REAL 2); :: thesis: for f being S-Sequence_in_R2 st p in rng f & p .. f <> 1 holds
f -: p is being_S-Seq
let f be S-Sequence_in_R2; :: thesis: ( p in rng f & p .. f <> 1 implies f -: p is being_S-Seq )
assume that
A1: p in rng f and
A2: p .. f <> 1 ; :: thesis: f -: p is being_S-Seq
thus f -: p is one-to-one ; :: according to TOPREAL1:def 8 :: thesis: ( 2 <= len (f -: p) & f -: p is unfolded & f -: p is s.n.c. & f -: p is special )
1 <= p .. f by A1, FINSEQ_4:21;
then 1 < p .. f by A2, XXREAL_0:1;
then 1 + 1 <= p .. f by NAT_1:13;
hence len (f -: p) >= 2 by A1, FINSEQ_5:42; :: thesis: ( f -: p is unfolded & f -: p is s.n.c. & f -: p is special )
thus ( f -: p is unfolded & f -: p is s.n.c. & f -: p is special ) ; :: thesis: verum