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_S-Seq_joining f /. 1,g /. (len g) )
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_S-Seq_joining f /. 1,g /. (len g)
then A2: (mid f,1,((len f) -' 1)) ^ g is being_S-Seq by Th80;
A3: ( f is one-to-one & len f >= 2 & f is unfolded & f is s.n.c. & f is special ) by A1, TOPREAL1:def 10;
A4: ( g is one-to-one & len g >= 2 & g is unfolded & g is s.n.c. & g is special ) by A1, TOPREAL1:def 10;
A5: 1 <= len f by A3, XXREAL_0:2;
A6: 1 <= len g by A4, XXREAL_0:2;
A7: (len f) -' 1 <= len f by NAT_D:50;
(1 + 1) - 1 <= (len f) - 1 by A3, XREAL_1:11;
then A8: 1 <= (len f) -' 1 by NAT_D:39;
A9: len ((mid f,1,((len f) -' 1)) ^ g) = (len (mid f,1,((len f) -' 1))) + (len g) by FINSEQ_1:35;
len (mid f,1,((len f) -' 1)) = (((len f) -' 1) -' 1) + 1 by A5, A7, A8, Th27
.= (((len f) -' 1) - 1) + 1 by A8, XREAL_1:235
.= (len f) -' 1 ;
then A10: ((mid f,1,((len f) -' 1)) ^ g) . 1 = (mid f,1,((len f) -' 1)) . 1 by A8, FINSEQ_1:85
.= f . 1 by A7, A8, Th32
.= f /. 1 by A5, FINSEQ_4:24 ;
0 + (len (mid f,1,((len f) -' 1))) < (len g) + (len (mid f,1,((len f) -' 1))) by A4, XREAL_1:8;
then ((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 A9, Th15
.= g /. (len g) by A6, A9, FINSEQ_4:24 ;
hence (mid f,1,((len f) -' 1)) ^ g is_S-Seq_joining f /. 1,g /. (len g) by A2, A10, Def3; :: thesis: verum