theorem Th14: :: NAT_3:14

for b being Nat
for f being FinSequence of REAL holds Product (f |^ (b + 1)) = (Product (f |^ b)) * (Product f)