let f, g be FinSequence of (TOP-REAL 2); 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); ( 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
; (mid f,1,((len f) -' 1)) ^ (R_Cut g,p) is_S-Seq_joining f /. 1,p
len g >= 2
by A4, TOPREAL1:def 10;
then A7:
1 <= len g
by XXREAL_0:2;
R_Cut g,p is_S-Seq_joining g /. 1,p
by A2, A4, A6, Th67;
then A8:
(R_Cut g,p) . 1 = g /. 1
by Def3;
then A9:
(R_Cut g,p) . 1 = f . (len f)
by A1, A7, FINSEQ_4:24;
A10:
len f >= 2
by A3, TOPREAL1:def 10;
then A11:
1 <= len f
by XXREAL_0:2;
A12:
(1 + 1) - 1 <= (len f) - 1
by A10, XREAL_1:11;
A13:
((len f) -' 1) + 1 = len f
by A10, XREAL_1:237, XXREAL_0:2;
then
f /. (len f) in LSeg (f /. ((len f) -' 1)),(f /. (((len f) -' 1) + 1))
by RLTOPSP1:69;
then
f /. (len f) in LSeg f,((len f) -' 1)
by A12, A13, TOPREAL1:def 5;
then
f . (len f) in LSeg f,((len f) -' 1)
by A11, FINSEQ_4:24;
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, Th70;
then A16:
1 + 1 <= len (R_Cut g,p)
by TOPREAL1:def 10;
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:24;
then A18:
(R_Cut g,p) /. (len (R_Cut g,p)) = p
by A2, Th59;
(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 A17, FINSEQ_4:24;
then
(R_Cut g,p) . 1 in LSeg (R_Cut g,p),1
by A16, TOPREAL1:def 5;
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:24;
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:37;
L~ (R_Cut g,p) c= L~ g
by A2, 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, 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, Th81; verum