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) and
A3: ( p `1 = (f /. (len f)) `1 or p `2 = (f /. (len f)) `2 ) and
A4: (LSeg p,(f /. (len f))) /\ (L~ f) = {(f /. (len f))} ; :: thesis: f ^ <*p*> is S-Sequence_in_R2
set g = <*(f /. (len f)),p*>;
reconsider f' = f as S-Sequence_in_R2 by A1;
A5: len f' in dom f' by FINSEQ_5:6;
A6: len <*(f /. (len f)),p*> = 1 + 1 by FINSEQ_1:61;
A7: <*(f /. (len f)),p*> . 1 = f /. (len f) by FINSEQ_1:61
.= f . (len f) by A5, PARTFUN1:def 8 ;
A8: <*(f /. (len f)),p*> is being_S-Seq by A2, A3, SPPOL_2:46;
A9: (L~ f) /\ (L~ <*(f /. (len f)),p*>) = {(f /. (len f))} by A4, SPPOL_2:21
.= {(f . (len f))} by A5, PARTFUN1:def 8 ;
mid <*(f /. (len f)),p*>,2,(len <*(f /. (len f)),p*>) = <*(<*(f /. (len f)),p*> /. 2)*> by A6, JORDAN4:27
.= <*p*> by FINSEQ_4:26 ;
hence f ^ <*p*> is S-Sequence_in_R2 by A1, A7, A8, A9, JORDAN3:73; :: thesis: verum