let p be Point of (TOP-REAL 2); :: thesis: for i being Element of NAT
for f being S-Sequence_in_R2 st p in LSeg f,i & not p in rng f holds
Ins f,i,p is being_S-Seq
let i be Element of NAT ; :: thesis: for f being S-Sequence_in_R2 st p in LSeg f,i & not p in rng f holds
Ins f,i,p is being_S-Seq
let f be S-Sequence_in_R2; :: thesis: ( p in LSeg f,i & not p in rng f implies Ins f,i,p is being_S-Seq )
assume that
A1: p in LSeg f,i and
A2: not p in rng f ; :: thesis: Ins f,i,p is being_S-Seq
set g = Ins f,i,p;
thus Ins f,i,p is one-to-one by A2, FINSEQ_5:79; :: according to TOPREAL1:def 10 :: thesis: ( 2 <= len (Ins f,i,p) & Ins f,i,p is unfolded & Ins f,i,p is s.n.c. & Ins f,i,p is special )
A3: len f >= 2 by TOPREAL1:def 10;
len (Ins f,i,p) = (len f) + 1 by FINSEQ_5:72;
then len (Ins f,i,p) >= len f by NAT_1:11;
hence len (Ins f,i,p) >= 2 by A3, XXREAL_0:2; :: thesis: ( Ins f,i,p is unfolded & Ins f,i,p is s.n.c. & Ins f,i,p is special )
thus Ins f,i,p is unfolded by A1, Th33; :: thesis: ( Ins f,i,p is s.n.c. & Ins f,i,p is special )
thus Ins f,i,p is s.n.c. by A1, A2, Th38; :: thesis: Ins f,i,p is special
thus Ins f,i,p is special by A1, Th44; :: thesis: verum