now

let i be Nat; :: thesis: ( i in dom (IdFinS p,n) implies (IdFinS p,n) . i in D )
assume A1: i in dom (IdFinS p,n) ; :: thesis: (IdFinS p,n) . i in D
i in Seg (len (IdFinS p,n)) by A1, 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