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 being_S-Seq )
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 being_S-Seq
A5:
Rev f is being_S-Seq
by A2;
L~ (Rev f) = L~ f
by SPPOL_2:22;
then A6:
(L~ (Rev g)) /\ (L~ (Rev f)) = {(g . 1)}
by A4, SPPOL_2:22;
A7:
(Rev f) . 1 = f . (len f)
by FINSEQ_5:62;
A8:
Rev g is being_S-Seq
by A3;
(Rev g) . (len (Rev g)) =
(Rev (Rev g)) . 1
by FINSEQ_5:62
.=
(Rev f) . 1
by A1, A7
;
then A9:
(Rev g) ^ (mid ((Rev f),2,(len (Rev f)))) is being_S-Seq
by A1, A5, A8, A6, A7, Th38;
A10:
(len f) -' 1 <= len f
by NAT_D:50;
A11:
len (Rev f) = len f
by FINSEQ_5:def 3;
A12:
len f >= 2
by A2, TOPREAL1:def 8;
then A13:
(len f) - 1 >= (1 + 1) - 1
by XREAL_1:9;
A14: ((len f) -' 1) + 1 =
((len f) - 1) + 1
by A12, XREAL_1:233, XXREAL_0:2
.=
len f
;
A15: ((len f) -' ((len f) -' 1)) + 1 =
((len f) - ((len f) -' 1)) + 1
by NAT_D:50, XREAL_1:233
.=
((len f) - ((len f) - 1)) + 1
by A12, XREAL_1:233, XXREAL_0:2
.=
2
;
1 <= len f
by A12, XXREAL_0:2;
then
(Rev g) ^ (Rev (mid (f,1,((len f) -' 1)))) is being_S-Seq
by A13, A10, A15, A11, A14, A9, FINSEQ_6:113;
then
Rev ((mid (f,1,((len f) -' 1))) ^ g) is being_S-Seq
by FINSEQ_5:64;
then
Rev (Rev ((mid (f,1,((len f) -' 1))) ^ g)) is being_S-Seq
;
hence
(mid (f,1,((len f) -' 1))) ^ g is being_S-Seq
; verum