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_S-Seq_joining p,g /. (len g)
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_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 A4, TOPREAL1:def 8;
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 A8, TOPREAL1:def 3;
then g . 1 in LSeg (g,1) by A9, FINSEQ_4:15;
then A10: g . 1 in L~ g by SPPOL_2:17;
L~ (L_Cut (f,p)) c= L~ f by A2, Th42;
then A11: (L~ (L_Cut (f,p))) /\ (L~ g) c= (L~ f) /\ (L~ g) by XBOOLE_1:27;
len f >= 2 by A3, TOPREAL1:def 8;
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 A14, XXREAL_0:2;
then (L_Cut (f,p)) . 1 = (L_Cut (f,p)) /. 1 by FINSEQ_4:15;
then A17: (L_Cut (f,p)) /. 1 = p by A2, Th23;
A18: ((len (L_Cut (f,p))) -' 1) + 1 = len (L_Cut (f,p)) by A14, XREAL_1:235, XXREAL_0:2;
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 A16, FINSEQ_4:15;
then (L_Cut (f,p)) . (len (L_Cut (f,p))) in LSeg ((L_Cut (f,p)),((len (L_Cut (f,p))) -' 1)) by A15, A18, TOPREAL1:def 3;
then f /. (len f) in L~ (L_Cut (f,p)) by A7, SPPOL_2:17;
then f . (len f) in L~ (L_Cut (f,p)) by A12, FINSEQ_4:15;
then g . 1 in (L~ (L_Cut (f,p))) /\ (L~ g) by A1, A10, XBOOLE_0:def 4;
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 A5, A11, XBOOLE_0:def 10;
hence (L_Cut (f,p)) ^ (mid (g,2,(len g))) is_S-Seq_joining p,g /. (len g) by A1, A4, A12, A13, A7, A17, Th39, FINSEQ_4:15; :: thesis: verum