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