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

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