set p = (Seg n) --> the Element of D;
dom ((Seg n) --> the Element of D) = Seg n ;
then reconsider p = (Seg n) --> the Element of D as FinSequence by FINSEQ_1:def 2;
take p ; :: thesis: ( p is D -valued & p is n -element )
thus rng p c= D by RELAT_1:def 19; :: according to RELAT_1:def 19 :: thesis: p is n -element
Seg (len p) = dom p by FINSEQ_1:def 3;
hence p is n -element by CARD_1:def 7, FINSEQ_1:6; :: thesis: verum