theorem :: POWER:41

for a being Real
for n being Nat holds a to_power n = a |^ n ;