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 f ^ (mid g,2,(len 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: f ^ (mid g,2,(len g)) is_S-Seq_joining f /. 1,g /. (len g)
then A2: f ^ (mid g,2,(len g)) is being_S-Seq by Th73;
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 ^ (mid g,2,(len g))) = (len f) + (len (mid g,2,(len g))) by FINSEQ_1:35;
A8: len (mid g,2,(len g)) = ((len g) -' 2) + 1 by A4, A6, Th27;
then A9: len (mid g,2,(len g)) = ((len g) - 2) + 1 by A4, XREAL_1:235
.= (len g) - 1 ;
A10: (1 + 1) - 1 <= (len g) - 1 by A4, XREAL_1:11;
A11: ((len (mid g,2,(len g))) + 2) - 1 = len g by A9;
A12: (f ^ (mid g,2,(len g))) . 1 = f . 1 by A5, FINSEQ_1:85
.= f /. 1 by A5, FINSEQ_4:24 ;
(len g) - 1 >= (1 + 1) - 1 by A4, XREAL_1:11;
then (len f) + 1 <= len (f ^ (mid g,2,(len g))) by A7, A9, 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 Th15
.= g . (len g) by A4, A7, A8, A10, A11, Th31
.= g /. (len g) by A6, FINSEQ_4:24 ;
hence f ^ (mid g,2,(len g)) is_S-Seq_joining f /. 1,g /. (len g) by A2, A12, Def3; :: thesis: verum