theorem Th23: :: FLEXARY1:23

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