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 A1: x = -infty ; :: thesis: (- 1) * x = - x

hence (- 1) * x = +infty by Def5
.= - x by A1, Def3 ;
:: thesis: verum

end;

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

hence (- 1) * x = -infty by Def5
.= - x by A2, Def3 ;
:: thesis: verum

end;

end;