now :: thesis: for i being Nat st i in dom (IdFinS (p,n)) holds

(IdFinS (p,n)) . i in D

hence
IdFinS (p,n) is FinSequence of D
by FINSEQ_2:12; :: thesis: verum(IdFinS (p,n)) . i in D

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 CARD_1:def 7;

then (IdFinS (p,n)) . i = p by FUNCOP_1:7;

hence (IdFinS (p,n)) . i in D ; :: thesis: verum

end;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 CARD_1:def 7;

then (IdFinS (p,n)) . i = p by FUNCOP_1:7;

hence (IdFinS (p,n)) . i in D ; :: thesis: verum