for n being Element of NAT
for r being Real st r > 0 holds
Product (n |-> r) = r to_power n