let f, g be FinSequence of (TOP-REAL 2); ( f . (len f) = g . 1 & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} implies (mid (f,1,((len f) -' 1))) ^ g is_S-Seq_joining f /. 1,g /. (len g) )
assume that
A1:
f . (len f) = g . 1
and
A2:
f is being_S-Seq
and
A3:
g is being_S-Seq
and
A4:
(L~ f) /\ (L~ g) = {(g . 1)}
; (mid (f,1,((len f) -' 1))) ^ g is_S-Seq_joining f /. 1,g /. (len g)
A5:
(len f) -' 1 <= len f
by NAT_D:50;
A6:
len f >= 2
by A2, TOPREAL1:def 8;
then
(1 + 1) - 1 <= (len f) - 1
by XREAL_1:9;
then A7:
1 <= (len f) -' 1
by NAT_D:39;
A8:
1 <= len f
by A6, XXREAL_0:2;
then len (mid (f,1,((len f) -' 1))) =
(((len f) -' 1) -' 1) + 1
by A5, A7, FINSEQ_6:118
.=
(((len f) -' 1) - 1) + 1
by A7, XREAL_1:233
.=
(len f) -' 1
;
then A9: ((mid (f,1,((len f) -' 1))) ^ g) . 1 =
(mid (f,1,((len f) -' 1))) . 1
by A7, FINSEQ_1:64
.=
f . 1
by A5, A7, FINSEQ_6:123
.=
f /. 1
by A8, FINSEQ_4:15
;
A10:
len ((mid (f,1,((len f) -' 1))) ^ g) = (len (mid (f,1,((len f) -' 1)))) + (len g)
by FINSEQ_1:22;
A11:
len g >= 2
by A3, TOPREAL1:def 8;
then A12:
1 <= len g
by XXREAL_0:2;
0 + (len (mid (f,1,((len f) -' 1)))) < (len g) + (len (mid (f,1,((len f) -' 1))))
by A11, XREAL_1:6;
then A13: ((mid (f,1,((len f) -' 1))) ^ g) . (len ((mid (f,1,((len f) -' 1))) ^ g)) =
g . ((len ((mid (f,1,((len f) -' 1))) ^ g)) - (len (mid (f,1,((len f) -' 1)))))
by A10, FINSEQ_6:108
.=
g /. (len g)
by A12, A10, FINSEQ_4:15
;
(mid (f,1,((len f) -' 1))) ^ g is being_S-Seq
by A1, A2, A3, A4, Th45;
hence
(mid (f,1,((len f) -' 1))) ^ g is_S-Seq_joining f /. 1,g /. (len g)
by A9, A13; verum