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