let p be Point of (TOP-REAL 2); :: thesis: for f being S-Sequence_in_R2 st p in rng f & p .. f <> len f holds
f :- p is being_S-Seq
let f be S-Sequence_in_R2; :: thesis: ( p in rng f & p .. f <> len f implies f :- p is being_S-Seq )
assume that
A1: p in rng f and
A2: p .. f <> len f ; :: thesis: f :- p is being_S-Seq
thus f :- p is one-to-one by A1, FINSEQ_5:59; :: according to TOPREAL1:def 10 :: thesis: ( 2 <= len (f :- p) & f :- p is unfolded & f :- p is s.n.c. & f :- p is special )

hereby :: thesis: ( f :- p is unfolded & f :- p is s.n.c. & f :- p is special )

p .. f <= len f by A1, FINSEQ_4:31;
then p .. f < len f by A2, XXREAL_0:1;
then 1 + (p .. f) <= len f by NAT_1:13;
then A3: (len f) - (p .. f) >= 1 by XREAL_1:21;
assume len (f :- p) < 2 ; :: thesis: contradiction
then ((len f) - (p .. f)) + 1 < 1 + 1 by A1, FINSEQ_5:53;
hence contradiction by A3, XREAL_1:8; :: thesis: verum

end;

thus ( f :- p is unfolded & f :- p is s.n.c. & f :- p is special ) by A1, Th28, Th35, Th41; :: thesis: verum