theorem Th81: :: XXREAL_3:81

for x being ExtReal holds 1 * x = x