for r, s being Real holds r |^ <*s*> = <*(r to_power s)*>