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 that
A1: f . (len f) = g . 1 and
A2: p in L~ g and
A3: f is being_S-Seq and
A4: g is being_S-Seq and
A5: (L~ f) /\ (L~ g) = {(g . 1)} and
A6: p <> g . 1 ; :: thesis: (mid (f,1,((len f) -' 1))) ^ (R_Cut (g,p)) is being_S-Seq
(mid (f,1,((len f) -' 1))) ^ (R_Cut (g,p)) is_S-Seq_joining f /. 1,p by A1, A2, A3, A4, A5, A6, Th47;
hence (mid (f,1,((len f) -' 1))) ^ (R_Cut (g,p)) is being_S-Seq ; :: thesis: verum