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