A1: rng p c= D by FINSEQ_1:def 4;
rng ((m,n) -cut p) c= rng p by Th11;
then rng ((m,n) -cut p) c= D by A1;
hence (m,n) -cut p is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum