let f, g be FinSequence of (TOP-REAL 2); 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); ( 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 that
A1:
f . (len f) = g . 1
and
A2:
p in L~ f
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 <> f . (len f)
; (L_Cut (f,p)) ^ (mid (g,2,(len g))) is being_S-Seq
(L_Cut (f,p)) ^ (mid (g,2,(len g))) is_S-Seq_joining p,g /. (len g)
by A1, A2, A3, A4, A5, A6, Th43;
hence
(L_Cut (f,p)) ^ (mid (g,2,(len g))) is being_S-Seq
; verum