reconsider S = Seg (n + 1) as non empty set by FINSEQ_1:6;
A1: rng p c= D by FINSEQ_1:def 4;
A2: m in S by Th8;
len p = n + 1 by FINSEQ_2:109;
then m in dom p by A2, FINSEQ_1:def 3;
then p . m in rng p by FUNCT_1:def 5;
hence p . m is Element of D by A1; :: thesis: verum