theorem :: WSIERP_1:21

for a being Nat
for fp being FinSequence of NAT st a in dom fp holds
(Product fp) / (fp . a) is Element of NAT