now

let i be Nat; :: thesis: ( i in dom (IdFinS (p,n)) implies (IdFinS (p,n)) . i in D )
assume i in dom (IdFinS (p,n)) ; :: thesis: (IdFinS (p,n)) . i in D
then i in Seg (len (IdFinS (p,n))) by FINSEQ_1:def 3;
then i in Seg n by FINSEQ_1:def 18;
then (IdFinS (p,n)) . i = p by FUNCOP_1:13;
hence (IdFinS (p,n)) . i in D ; :: thesis: verum

end;

hence IdFinS (p,n) is FinSequence of D by FINSEQ_2:14; :: thesis: verum