let g be FinSequence of (TOP-REAL 2); 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); ( 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)}
; <*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; verum