for x being Real
for n being Nat holds |.(x |^ n).| = |.x.| |^ n