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)*>;
A5: <*p,(g /. 1)*> is being_S-Seq by A1, A2, SPPOL_2:43;
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 FINSEQ_3:25, A7;
then A8: mid (<*p,(g /. 1)*>,1,((len <*p,(g /. 1)*>) -' 1)) = <*(<*p,(g /. 1)*> . 1)*> by AB, FINSEQ_6:193
.= <*(<*p,(g /. 1)*> /. 1)*> by AA, PARTFUN1:def 6
.= <*p*> by FINSEQ_4:17 ;
A9: (L~ <*p,(g /. 1)*>) /\ (L~ g) = {(g /. 1)} by A4, SPPOL_2:21
.= {(g . 1)} by A6, PARTFUN1:def 6 ;
<*p,(g /. 1)*> . (len <*p,(g /. 1)*>) = g /. 1 by A7
.= g . 1 by A6, PARTFUN1:def 6 ;
hence <*p*> ^ g is being_S-Seq by A3, A5, A9, A8, JORDAN3:45; :: thesis: verum