let x be ext-real number ; :: 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 number ;
2 * x = x + x ;
hence 2 * x = x + x ; :: thesis: verum

end;

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

hence 2 * x = -infty by Def4
.= x + x by S, Def3 ;
:: thesis: verum

end;

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

hence 2 * x = +infty by Def4
.= x + x by S, Def3 ;
:: thesis: verum

end;

end;