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~ g & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} & p <> g . 1 holds
(mid f,1,((len f) -' 1)) ^ (R_Cut g,p) is being_S-Seq
let p be Point of (TOP-REAL 2); :: thesis: ( f . (len f) = g . 1 & p in L~ g & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} & p <> g . 1 implies (mid f,1,((len f) -' 1)) ^ (R_Cut g,p) is being_S-Seq )
assume ( f . (len f) = g . 1 & p in L~ g & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} & p <> g . 1 ) ; :: thesis: (mid f,1,((len f) -' 1)) ^ (R_Cut g,p) is being_S-Seq
then (mid f,1,((len f) -' 1)) ^ (R_Cut g,p) is_S-Seq_joining f /. 1,p by Th82;
hence (mid f,1,((len f) -' 1)) ^ (R_Cut g,p) is being_S-Seq by Def3; :: thesis: verum