theorem Th12: :: NAT_3:12

for a being Nat
for r being Real holds <*r*> |^ a = <*(r |^ a)*>