let f, g be FinSequence of (); :: thesis: for p being Point of () 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_S-Seq_joining p,g /. (len g)

let p be Point of (); :: 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_S-Seq_joining p,g /. (len g) )
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) ; :: thesis: (L_Cut (f,p)) ^ (mid (g,2,(len g))) is_S-Seq_joining p,g /. (len g)
L_Cut (f,p) is_S-Seq_joining p,f /. (len f) by A2, A3, A6, Th33;
then A7: (L_Cut (f,p)) . (len (L_Cut (f,p))) = f /. (len f) ;
A8: len g >= 2 by ;
then A9: 1 <= len g by XXREAL_0:2;
g /. 1 in LSeg ((g /. 1),(g /. (1 + 1))) by RLTOPSP1:68;
then g /. 1 in LSeg (g,1) by ;
then g . 1 in LSeg (g,1) by ;
then A10: g . 1 in L~ g by SPPOL_2:17;
L~ (L_Cut (f,p)) c= L~ f by ;
then A11: (L~ (L_Cut (f,p))) /\ (L~ g) c= (L~ f) /\ (L~ g) by XBOOLE_1:27;
len f >= 2 by ;
then A12: 1 <= len f by XXREAL_0:2;
A13: L_Cut (f,p) is being_S-Seq by A2, A3, A6, Th34;
then A14: 1 + 1 <= len (L_Cut (f,p)) by TOPREAL1:def 8;
then A15: (1 + 1) - 1 <= (len (L_Cut (f,p))) - 1 by XREAL_1:9;
A16: 1 <= len (L_Cut (f,p)) by ;
then (L_Cut (f,p)) . 1 = (L_Cut (f,p)) /. 1 by FINSEQ_4:15;
then A17: (L_Cut (f,p)) /. 1 = p by ;
A18: ((len (L_Cut (f,p))) -' 1) + 1 = len (L_Cut (f,p)) by ;
then (L_Cut (f,p)) /. (len (L_Cut (f,p))) in LSeg (((L_Cut (f,p)) /. ((len (L_Cut (f,p))) -' 1)),((L_Cut (f,p)) /. (((len (L_Cut (f,p))) -' 1) + 1))) by RLTOPSP1:68;
then (L_Cut (f,p)) . (len (L_Cut (f,p))) in LSeg (((L_Cut (f,p)) /. ((len (L_Cut (f,p))) -' 1)),((L_Cut (f,p)) /. (((len (L_Cut (f,p))) -' 1) + 1))) by ;
then (L_Cut (f,p)) . (len (L_Cut (f,p))) in LSeg ((L_Cut (f,p)),((len (L_Cut (f,p))) -' 1)) by ;
then f /. (len f) in L~ (L_Cut (f,p)) by ;
then f . (len f) in L~ (L_Cut (f,p)) by ;
then g . 1 in (L~ (L_Cut (f,p))) /\ (L~ g) by ;
then {(g . 1)} c= (L~ (L_Cut (f,p))) /\ (L~ g) by ZFMISC_1:31;
then (L~ (L_Cut (f,p))) /\ (L~ g) = {(g . 1)} by ;
hence (L_Cut (f,p)) ^ (mid (g,2,(len g))) is_S-Seq_joining p,g /. (len g) by ; :: thesis: verum