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, Th68;
then A7: (L_Cut f,p) . (len (L_Cut f,p)) = f /. (len f) by Def3;
A8: len g >= 2 by A4, TOPREAL1:def 10;
then A9: 1 <= len g by XXREAL_0:2;
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 A9, FINSEQ_4:24;
then A10: g . 1 in L~ g by SPPOL_2:17;
L~ (L_Cut f,p) c= L~ f by A2, Th77;
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 10;
then A12: 1 <= len f by XXREAL_0:2;
A13: L_Cut f,p is being_S-Seq by A2, A3, A6, Th69;
then A14: 1 + 1 <= len (L_Cut f,p) by TOPREAL1:def 10;
then A15: (1 + 1) - 1 <= (len (L_Cut f,p)) - 1 by XREAL_1:11;
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:24;
then A17: (L_Cut f,p) /. 1 = p by A2, Th58;
A18: ((len (L_Cut f,p)) -' 1) + 1 = len (L_Cut f,p) by A14, 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 A16, 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 A15, A18, TOPREAL1:def 5;
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:24;
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:37;
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, Th74, FINSEQ_4:24; :: thesis: verum