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:56; :: according to TOPREAL1:def 8 :: thesis: ( 2 <= len (f :- p) & f :- p is unfolded & f :- p is s.n.c. & f :- p is special )

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:56; :: according to TOPREAL1:def 8 :: 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 )

thus
( f :- p is unfolded & f :- p is s.n.c. & f :- p is special )
by A1, Th27, Th34, Th39; :: thesis: verum
p .. f <= len f
by A1, FINSEQ_4:21;

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:19;

assume len (f :- p) < 2 ; :: thesis: contradiction

then ((len f) - (p .. f)) + 1 < 1 + 1 by A1, FINSEQ_5:50;

hence contradiction by A3, XREAL_1:6; :: thesis: verum

end;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:19;

assume len (f :- p) < 2 ; :: thesis: contradiction

then ((len f) - (p .. f)) + 1 < 1 + 1 by A1, FINSEQ_5:50;

hence contradiction by A3, XREAL_1:6; :: thesis: verum