( mid (f,k1,k2) = (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) or mid (f,k1,k2) = Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) ) by Def3;
hence mid (f,k1,k2) is FinSequence of D ; :: thesis: verum