rng fp c= NAT by VALUED_0:def 6;
then reconsider fp = fp as FinSequence of NAT by FINSEQ_1:def 4;
Product fp in NAT ;
hence Product fp is natural ; :: thesis: verum