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) holds
L_Cut (f,p) = <*p*>
let p be Point of (TOP-REAL 2); ( f is being_S-Seq & p = f . (len f) implies L_Cut (f,p) = <*p*> )
assume that
A1:
f is being_S-Seq
and
A2:
p = f . (len f)
; L_Cut (f,p) = <*p*>
len f >= 2
by A1, TOPREAL1:def 8;
then
p in L~ f
by A2, JORDAN3:1;
then A3:
p in L~ (Rev f)
by SPPOL_2:22;
A4: L_Cut (f,p) =
L_Cut ((Rev (Rev f)),p)
.=
Rev (R_Cut ((Rev f),p))
by A1, A3, JORDAN3:22
;
p = (Rev f) . 1
by A2, FINSEQ_5:62;
then
R_Cut ((Rev f),p) = <*p*>
by JORDAN3:def 4;
hence
L_Cut (f,p) = <*p*>
by A4, FINSEQ_5:60; verum