theorem PRA: :: NEWTON04:62

for n being Nat
for a being Real holds Product ((a,a) Subnomial n) = a |^ (n * (n + 1))