let x be ExtReal; :: thesis: 1 * x = x

per cases ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14;

suppose x in REAL ; :: thesis: 1 * x = x

then reconsider x = x, y = 1 as Real ;
y * x = x ;
hence 1 * x = x ; :: thesis: verum

end;

suppose ( x = -infty or x = +infty ) ; :: thesis: 1 * x = x

hence 1 * x = x by Def5; :: thesis: verum

end;

end;