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, Th38;
A6:
len g >= 2
by A3, TOPREAL1:def 8;
then A7:
(1 + 1) - 1 <= (len g) - 1
by XREAL_1:9;
len f >= 2
by A2, TOPREAL1:def 8;
then A8:
1 <= len f
by XXREAL_0:2;
then A9: (f ^ (mid (g,2,(len g)))) . 1 =
f . 1
by FINSEQ_1:64
.=
f /. 1
by A8, FINSEQ_4:15
;
A10:
len (f ^ (mid (g,2,(len g)))) = (len f) + (len (mid (g,2,(len g))))
by FINSEQ_1:22;
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:118;
then A13: len (mid (g,2,(len g))) =
((len g) - 2) + 1
by A6, XREAL_1:233
.=
(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:9;
then
(len f) + 1 <= len (f ^ (mid (g,2,(len g))))
by A10, A13, XREAL_1:6;
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:108
.=
g . (len g)
by A6, A10, A12, A7, A14, FINSEQ_6:122
.=
g /. (len g)
by A11, FINSEQ_4:15
;
hence
f ^ (mid (g,2,(len g))) is_S-Seq_joining f /. 1,g /. (len g)
by A5, A9; verum