for x being Element of ExtREAL
for y being Real
for k being Nat st x = y holds
x |^ k = y |^ k