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 10;
then
(1 + 1) - 1 <= (len f) - 1
by XREAL_1:11;
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:124
.=
(((len f) -' 1) - 1) + 1
by A7, XREAL_1:235
.=
(len f) -' 1
;
then A9: ((mid f,1,((len f) -' 1)) ^ g) . 1 =
(mid f,1,((len f) -' 1)) . 1
by A7, FINSEQ_1:85
.=
f . 1
by A5, A7, FINSEQ_6:129
.=
f /. 1
by A8, FINSEQ_4:24
;
A10:
len ((mid f,1,((len f) -' 1)) ^ g) = (len (mid f,1,((len f) -' 1))) + (len g)
by FINSEQ_1:35;
A11:
len g >= 2
by A3, TOPREAL1:def 10;
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:8;
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:114
.=
g /. (len g)
by A12, A10, FINSEQ_4:24
;
(mid f,1,((len f) -' 1)) ^ g is being_S-Seq
by A1, A2, A3, A4, Th80;
hence
(mid f,1,((len f) -' 1)) ^ g is_S-Seq_joining f /. 1,g /. (len g)
by A9, A13, Def3; verum