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

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