theorem Th39: :: POLYDIFF:39

for n being Nat
for r being Element of F_Real holds power (r,n) = r |^ n