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