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

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