for x being Element of ExtREAL
for k being Nat st 0 <= x holds
0 <= x |^ k