theorem Th9: :: MESFUNC7:9

for x being Element of ExtREAL holds x |^ 1 = x