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)
A7: ( f is one-to-one & len f >= 2 & f is unfolded & f is s.n.c. & f is special ) by A3, TOPREAL1:def 10;
A8: ( g is one-to-one & len g >= 2 & g is unfolded & g is s.n.c. & g is special ) by A4, TOPREAL1:def 10;
A9: 1 <= len f by A7, XXREAL_0:2;
A10: 1 <= len g by A8, XXREAL_0:2;
A11: L_Cut f,p is being_S-Seq by A2, A3, A6, Th69;
then A12: 1 + 1 <= len (L_Cut f,p) by TOPREAL1:def 10;
then A13: (1 + 1) - 1 <= (len (L_Cut f,p)) - 1 by XREAL_1:11;
L_Cut f,p is_S-Seq_joining p,f /. (len f) by A2, A3, A6, Th68;
then A14: ( (L_Cut f,p) . 1 = p & (L_Cut f,p) . (len (L_Cut f,p)) = f /. (len f) ) by Def3;
A15: 1 <= len (L_Cut f,p) by A12, XXREAL_0:2;
then (L_Cut f,p) . 1 = (L_Cut f,p) /. 1 by FINSEQ_4:24;
then A16: (L_Cut f,p) /. 1 = p by A2, Th58;
g /. 1 in LSeg (g /. 1),(g /. (1 + 1)) by RLTOPSP1:69;
then g /. 1 in LSeg g,1 by A8, TOPREAL1:def 5;
then g . 1 in LSeg g,1 by A10, FINSEQ_4:24;
then A17: g . 1 in L~ g by SPPOL_2:17;
A18: ((len (L_Cut f,p)) -' 1) + 1 = len (L_Cut f,p) by A12, XREAL_1:237, 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:69;
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 A15, FINSEQ_4:24;
then (L_Cut f,p) . (len (L_Cut f,p)) in LSeg (L_Cut f,p),((len (L_Cut f,p)) -' 1) by A13, A18, TOPREAL1:def 5;
then f /. (len f) in L~ (L_Cut f,p) by A14, SPPOL_2:17;
then f . (len f) in L~ (L_Cut f,p) by A9, FINSEQ_4:24;
then g . 1 in (L~ (L_Cut f,p)) /\ (L~ g) by A1, A17, XBOOLE_0:def 4;
then A19: {(g . 1)} c= (L~ (L_Cut f,p)) /\ (L~ g) by ZFMISC_1:37;
L~ (L_Cut f,p) c= L~ f by A2, Th77;
then (L~ (L_Cut f,p)) /\ (L~ g) c= (L~ f) /\ (L~ g) by XBOOLE_1:27;
then (L~ (L_Cut f,p)) /\ (L~ g) = {(g . 1)} by A5, A19, 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, A9, A11, A14, A16, Th74, FINSEQ_4:24; :: thesis: verum