let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & p <> f . (len f) holds
L_Cut f,p is being_S-Seq
let p be Point of (TOP-REAL 2); :: thesis: ( f is being_S-Seq & p in L~ f & p <> f . (len f) implies L_Cut f,p is being_S-Seq )
assume ( f is being_S-Seq & p in L~ f & p <> f . (len f) ) ; :: thesis: L_Cut f,p is being_S-Seq
then L_Cut f,p is_S-Seq_joining p,f /. (len f) by Th68;
hence L_Cut f,p is being_S-Seq by Def3; :: thesis: verum