for z being Complex
for k being Nat holds
( z |^ (2 * k) = (z |^ k) |^ 2 & z |^ (2 * k) = (z |^ 2) |^ k )