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