now :: thesis: for i being Nat st i in dom (IdFinS (p,n)) holds
(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;
hence IdFinS (p,n) is FinSequence of D by FINSEQ_2:12; :: thesis: verum