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