A1: rng p c= D by FINSEQ_1:def 4;
A2: n is Element of NAT by ORDINAL1:def 13;
m is Element of NAT by ORDINAL1:def 13;
then rng (m,n -cut p) c= rng p by A2, Th11;
then rng (m,n -cut p) c= D by A1, XBOOLE_1:1;
hence m,n -cut p is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum