for x being Element of ExtREAL
for k being Nat holds x |^ (k + 1) = (x |^ k) * x