reconsider S = Seg (n + 1) as non empty set by FINSEQ_1:4;
( m in S & len p = n + 1 ) by Th7, CARD_1:def 7;
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 3;
hence p . m is Element of D ; :: thesis: verum