let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( 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 A1: ( f . (len f) = g . 1 & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} ) ; :: thesis: (mid f,1,((len f) -' 1)) ^ g is being_S-Seq
then A2: ( f is one-to-one & len f >= 2 & f is unfolded & f is s.n.c. & f is special ) by TOPREAL1:def 10;
then A3: 1 <= len f by XXREAL_0:2;
A4: (len f) - 1 >= (1 + 1) - 1 by A2, XREAL_1:11;
A5: Rev f is being_S-Seq by A1, SPPOL_2:47;
A6: Rev g is being_S-Seq by A1, SPPOL_2:47;
L~ (Rev f) = L~ f by SPPOL_2:22;
then A7: (L~ (Rev g)) /\ (L~ (Rev f)) = {(g . 1)} by A1, SPPOL_2:22;
A8: (Rev f) . 1 = f . (len f) by FINSEQ_5:65;
A9: (Rev g) . (len (Rev g)) = (Rev (Rev g)) . 1 by FINSEQ_5:65
.= (Rev f) . 1 by A1, A8, FINSEQ_6:29 ;
A10: (len f) -' 1 <= len f by NAT_D:50;
A11: ((len f) -' ((len f) -' 1)) + 1 = ((len f) - ((len f) -' 1)) + 1 by NAT_D:50, XREAL_1:235
.= ((len f) - ((len f) - 1)) + 1 by A2, XREAL_1:235, XXREAL_0:2
.= 2 ;
A12: len (Rev f) = len f by FINSEQ_5:def 3;
A13: ((len f) -' 1) + 1 = ((len f) - 1) + 1 by A2, XREAL_1:235, XXREAL_0:2
.= len f ;
(Rev g) ^ (mid (Rev f),2,(len (Rev f))) is being_S-Seq by A1, A5, A6, A7, A8, A9, Th73;
then (Rev g) ^ (Rev (mid f,1,((len f) -' 1))) is being_S-Seq by A3, A4, A10, A11, A12, A13, Th22;
then Rev ((mid f,1,((len f) -' 1)) ^ g) is being_S-Seq by FINSEQ_5:67;
then Rev (Rev ((mid f,1,((len f) -' 1)) ^ g)) is being_S-Seq by SPPOL_2:47;
hence (mid f,1,((len f) -' 1)) ^ g is being_S-Seq by FINSEQ_6:29; :: thesis: verum