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