let f be FinSequence of (TOP-REAL 2); for p being Point of (TOP-REAL 2) st f is being_S-Seq & p <> f /. (len f) & ( p `1 = (f /. (len f)) `1 or p `2 = (f /. (len f)) `2 ) & (LSeg (p,(f /. (len f)))) /\ (L~ f) = {(f /. (len f))} holds
f ^ <*p*> is S-Sequence_in_R2
let p be Point of (TOP-REAL 2); ( f is being_S-Seq & p <> f /. (len f) & ( p `1 = (f /. (len f)) `1 or p `2 = (f /. (len f)) `2 ) & (LSeg (p,(f /. (len f)))) /\ (L~ f) = {(f /. (len f))} implies f ^ <*p*> is S-Sequence_in_R2 )
assume that
A1:
f is being_S-Seq
and
A2:
( p <> f /. (len f) & ( p `1 = (f /. (len f)) `1 or p `2 = (f /. (len f)) `2 ) )
and
A3:
(LSeg (p,(f /. (len f)))) /\ (L~ f) = {(f /. (len f))}
; f ^ <*p*> is S-Sequence_in_R2
set g = <*(f /. (len f)),p*>;
A4:
<*(f /. (len f)),p*> is being_S-Seq
by A2, SPPOL_2:43;
AB:
len <*(f /. (len f)),p*> = 1 + 1
by FINSEQ_1:44;
then AA:
2 in dom <*(f /. (len f)),p*>
by FINSEQ_3:25;
then A5: mid (<*(f /. (len f)),p*>,2,(len <*(f /. (len f)),p*>)) =
<*(<*(f /. (len f)),p*> . 2)*>
by JORDAN4:15, AB
.=
<*(<*(f /. (len f)),p*> /. 2)*>
by AA, PARTFUN1:def 6
.=
<*p*>
by FINSEQ_4:17
;
reconsider f9 = f as S-Sequence_in_R2 by A1;
A6:
len f9 in dom f9
by FINSEQ_5:6;
A7: <*(f /. (len f)),p*> . 1 =
f /. (len f)
by FINSEQ_1:44
.=
f . (len f)
by A6, PARTFUN1:def 6
;
(L~ f) /\ (L~ <*(f /. (len f)),p*>) =
{(f /. (len f))}
by A3, SPPOL_2:21
.=
{(f . (len f))}
by A6, PARTFUN1:def 6
;
hence
f ^ <*p*> is S-Sequence_in_R2
by A1, A7, A4, A5, JORDAN3:38; verum