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

(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