let g be FinSequence of (); :: thesis: for p being Point of () st g /. 1 <> p & ( (g /. 1) `1 = p `1 or (g /. 1) `2 = p `2 ) & g is being_S-Seq & (LSeg (p,(g /. 1))) /\ (L~ g) = {(g /. 1)} holds
<*p*> ^ g is being_S-Seq

let p be Point of (); :: thesis: ( g /. 1 <> p & ( (g /. 1) `1 = p `1 or (g /. 1) `2 = p `2 ) & g is being_S-Seq & (LSeg (p,(g /. 1))) /\ (L~ g) = {(g /. 1)} implies <*p*> ^ g is being_S-Seq )
assume that
A1: g /. 1 <> p and
A2: ( (g /. 1) `1 = p `1 or (g /. 1) `2 = p `2 ) and
A3: g is being_S-Seq and
A4: (LSeg (p,(g /. 1))) /\ (L~ g) = {(g /. 1)} ; :: thesis: <*p*> ^ g is being_S-Seq
set f = <*p,(g /. 1)*>;
A5: <*p,(g /. 1)*> is being_S-Seq by ;
reconsider g9 = g as S-Sequence_in_R2 by A3;
A6: 1 in dom g9 by FINSEQ_5:6;
A7: len <*p,(g /. 1)*> = 1 + 1 by FINSEQ_1:44;
then AB: (len <*p,(g /. 1)*>) -' 1 = 1 by NAT_D:34;
AA: 1 in dom <*p,(g /. 1)*> by ;
then A8: mid (<*p,(g /. 1)*>,1,((len <*p,(g /. 1)*>) -' 1)) = <*(<*p,(g /. 1)*> . 1)*> by
.= <*(<*p,(g /. 1)*> /. 1)*> by
.= <*p*> by FINSEQ_4:17 ;
A9: (L~ <*p,(g /. 1)*>) /\ (L~ g) = {(g /. 1)} by
.= {(g . 1)} by ;
<*p,(g /. 1)*> . (len <*p,(g /. 1)*>) = g /. 1 by
.= g . 1 by ;
hence <*p*> ^ g is being_S-Seq by ; :: thesis: verum