smid (f,k1,k2) = (f /^ (k1 -' 1)) | ((k2 + 1) -' k1) ;
hence smid (f,k1,k2) is FinSequence of D ; :: thesis: verum