theorem Th54: :: NAT_4:55

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