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_S-Seq_joining f /. 1,p
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_S-Seq_joining f /. 1,p )
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_S-Seq_joining f /. 1,p
len g >= 2 by A4, TOPREAL1:def 8;
then A7: 1 <= len g by XXREAL_0:2;
R_Cut (g,p) is_S-Seq_joining g /. 1,p by A2, A4, A6, Th32;
then A8: (R_Cut (g,p)) . 1 = g /. 1 ;
then A9: (R_Cut (g,p)) . 1 = f . (len f) by A1, A7, FINSEQ_4:15;
A10: len f >= 2 by A3, TOPREAL1:def 8;
then A11: 1 <= len f by XXREAL_0:2;
A12: (1 + 1) - 1 <= (len f) - 1 by A10, XREAL_1:9;
A13: ((len f) -' 1) + 1 = len f by A10, XREAL_1:235, XXREAL_0:2;
then f /. (len f) in LSeg ((f /. ((len f) -' 1)),(f /. (((len f) -' 1) + 1))) by RLTOPSP1:68;
then f /. (len f) in LSeg (f,((len f) -' 1)) by A12, A13, TOPREAL1:def 3;
then f . (len f) in LSeg (f,((len f) -' 1)) by A11, FINSEQ_4:15;
then A14: f . (len f) in L~ f by SPPOL_2:17;
A15: R_Cut (g,p) is being_S-Seq by A2, A4, A6, Th35;
then A16: 1 + 1 <= len (R_Cut (g,p)) by TOPREAL1:def 8;
then A17: 1 <= len (R_Cut (g,p)) by XXREAL_0:2;
then (R_Cut (g,p)) . (len (R_Cut (g,p))) = (R_Cut (g,p)) /. (len (R_Cut (g,p))) by FINSEQ_4:15;
then A18: (R_Cut (g,p)) /. (len (R_Cut (g,p))) = p by A2, Th24;
(R_Cut (g,p)) /. 1 in LSeg (((R_Cut (g,p)) /. 1),((R_Cut (g,p)) /. (1 + 1))) by RLTOPSP1:68;
then (R_Cut (g,p)) . 1 in LSeg (((R_Cut (g,p)) /. 1),((R_Cut (g,p)) /. (1 + 1))) by A17, FINSEQ_4:15;
then (R_Cut (g,p)) . 1 in LSeg ((R_Cut (g,p)),1) by A16, TOPREAL1:def 3;
then g /. 1 in L~ (R_Cut (g,p)) by A8, SPPOL_2:17;
then g . 1 in L~ (R_Cut (g,p)) by A7, FINSEQ_4:15;
then f . (len f) in (L~ f) /\ (L~ (R_Cut (g,p))) by A1, A14, XBOOLE_0:def 4;
then A19: {(f . (len f))} c= (L~ f) /\ (L~ (R_Cut (g,p))) by ZFMISC_1:31;
L~ (R_Cut (g,p)) c= L~ g by A2, Th41;
then (L~ f) /\ (L~ (R_Cut (g,p))) c= (L~ f) /\ (L~ g) by XBOOLE_1:27;
then (L~ f) /\ (L~ (R_Cut (g,p))) = {((R_Cut (g,p)) . 1)} by A1, A5, A9, A19, XBOOLE_0:def 10;
hence (mid (f,1,((len f) -' 1))) ^ (R_Cut (g,p)) is_S-Seq_joining f /. 1,p by A3, A15, A9, A18, Th46; :: thesis: verum