let x be ExtReal; :: thesis: 2 * x = x + x

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

suppose x in REAL ; :: thesis: 2 * x = x + x

then reconsider x = x as Real ;
2 * x = x + x ;
hence 2 * x = x + x ; :: thesis: verum

end;

suppose A1: x = -infty ; :: thesis: 2 * x = x + x

hence 2 * x = -infty by Def5
.= x + x by A1, Def2 ;
:: thesis: verum

end;

suppose A2: x = +infty ; :: thesis: 2 * x = x + x

hence 2 * x = +infty by Def5
.= x + x by A2, Def2 ;
:: thesis: verum

end;

end;