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