theorem :: NAT_3:15

for a being Nat
for f being FinSequence of REAL holds Product (f |^ a) = (Product f) |^ a