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