let f, g be FinSequence; :: thesis: smid ((f ^ g),((len f) + 1),((len f) + (len g))) = g
(((len g) + (len f)) + 1) -' ((len f) + 1) = ((len g) + ((len f) + 1)) -' ((len f) + 1)
.= len g by NAT_D:34 ;
then g | ((((len g) + (len f)) + 1) -' ((len f) + 1)) = g by FINSEQ_1:58;
then ((f ^ g) /^ (len f)) | ((((len f) + (len g)) + 1) -' ((len f) + 1)) = g by FINSEQ_5:37;
hence smid ((f ^ g),((len f) + 1),((len f) + (len g))) = g by NAT_D:34; :: thesis: verum