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

( 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