let g be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) 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 (TOP-REAL 2); :: 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)*>;
reconsider g' = g as S-Sequence_in_R2 by A3;
A5: 1 in dom g' by FINSEQ_5:6;
A6: len <*p,(g /. 1)*> = 1 + 1 by FINSEQ_1:61;
then A7: (len <*p,(g /. 1)*>) -' 1 = 1 by NAT_D:34;
A8: <*p,(g /. 1)*> . (len <*p,(g /. 1)*>) = g /. 1 by A6, FINSEQ_1:61
.= g . 1 by A5, PARTFUN1:def 8 ;
A9: <*p,(g /. 1)*> is being_S-Seq by A1, A2, SPPOL_2:46;
A10: (L~ <*p,(g /. 1)*>) /\ (L~ g) = {(g /. 1)} by A4, SPPOL_2:21
.= {(g . 1)} by A5, PARTFUN1:def 8 ;
mid <*p,(g /. 1)*>,1,((len <*p,(g /. 1)*>) -' 1) = <*(<*p,(g /. 1)*> /. 1)*> by A6, A7, JORDAN4:27
.= <*p*> by FINSEQ_4:26 ;
hence <*p*> ^ g is being_S-Seq by A3, A8, A9, A10, JORDAN3:80; :: thesis: verum