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 A1: ( 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 ) ; :: thesis: (mid f,1,((len f) -' 1)) ^ (R_Cut g,p) is_S-Seq_joining f /. 1,p
then A2: ( f is one-to-one & len f >= 2 ) by TOPREAL1:def 10;
A3: ( g is one-to-one & len g >= 2 ) by A1, TOPREAL1:def 10;
A4: 1 <= len f by A2, XXREAL_0:2;
A5: 1 <= len g by A3, XXREAL_0:2;
A6: (1 + 1) - 1 <= (len f) - 1 by A2, XREAL_1:11;
A7: ((len f) -' 1) + 1 = len f by A2, XREAL_1:237, XXREAL_0:2;
A8: R_Cut g,p is being_S-Seq by A1, Th70;
then A9: 1 + 1 <= len (R_Cut g,p) by TOPREAL1:def 10;
R_Cut g,p is_S-Seq_joining g /. 1,p by A1, Th67;
then A10: ( (R_Cut g,p) . 1 = g /. 1 & (R_Cut g,p) . (len (R_Cut g,p)) = p ) by Def3;
then A11: (R_Cut g,p) . 1 = f . (len f) by A1, A5, FINSEQ_4:24;
A12: 1 <= len (R_Cut g,p) by A9, 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:24;
then A13: (R_Cut g,p) /. (len (R_Cut g,p)) = p by A1, Th59;
f /. (len f) in LSeg (f /. ((len f) -' 1)),(f /. (((len f) -' 1) + 1)) by A7, RLTOPSP1:69;
then f /. (len f) in LSeg f,((len f) -' 1) by A6, A7, TOPREAL1:def 5;
then f . (len f) in LSeg f,((len f) -' 1) by A4, FINSEQ_4:24;
then A14: f . (len f) in L~ f by SPPOL_2:17;
(R_Cut g,p) /. 1 in LSeg ((R_Cut g,p) /. 1),((R_Cut g,p) /. (1 + 1)) by RLTOPSP1:69;
then (R_Cut g,p) . 1 in LSeg ((R_Cut g,p) /. 1),((R_Cut g,p) /. (1 + 1)) by A12, FINSEQ_4:24;
then (R_Cut g,p) . 1 in LSeg (R_Cut g,p),1 by A9, TOPREAL1:def 5;
then g /. 1 in L~ (R_Cut g,p) by A10, SPPOL_2:17;
then g . 1 in L~ (R_Cut g,p) by A5, FINSEQ_4:24;
then f . (len f) in (L~ f) /\ (L~ (R_Cut g,p)) by A1, A14, XBOOLE_0:def 4;
then A15: {(f . (len f))} c= (L~ f) /\ (L~ (R_Cut g,p)) by ZFMISC_1:37;
L~ (R_Cut g,p) c= L~ g by A1, Th76;
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, A11, A15, XBOOLE_0:def 10;
hence (mid f,1,((len f) -' 1)) ^ (R_Cut g,p) is_S-Seq_joining f /. 1,p by A1, A8, A11, A13, Th81; :: thesis: verum