reconsider k11 = k1, k21 = k2 as Element of NAT by ORDINAL1:def 13;
mid f,k1,k2 = (f | k21) /^ (k11 -' 1) by AB540b;
hence mid f,k1,k2 is XFinSequence of ; :: thesis: verum