theorem Th11: :: MESFUNC7:11

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