let p be Point of (TOP-REAL 2); :: thesis: for i being 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 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:76; :: according to TOPREAL1:def 8 :: 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 )
len (Ins (f,i,p)) = (len f) + 1 by FINSEQ_5:69;
then A3: len (Ins (f,i,p)) >= len f by NAT_1:11;
len f >= 2 by TOPREAL1:def 8;
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, Th32; :: 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, Th37; :: thesis: Ins (f,i,p) is special
thus Ins (f,i,p) is special by A1, Th41; :: thesis: verum