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, JORDAN4:15

.= <*(<*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, FINSEQ_1:44

.= g . 1 by A6, PARTFUN1:def 6 ;

hence <*p*> ^ g is being_S-Seq by A3, A5, A9, A8, JORDAN3:45; :: thesis: verum

<*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, JORDAN4:15

.= <*(<*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, FINSEQ_1:44

.= g . 1 by A6, PARTFUN1:def 6 ;

hence <*p*> ^ g is being_S-Seq by A3, A5, A9, A8, JORDAN3:45; :: thesis: verum