let x be ExtReal; :: thesis: x + 0 = x

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

suppose x in REAL ; :: thesis: x + 0 = x

then reconsider r = x as Real ;
r + 0 = r ;
hence x + 0 = x ; :: thesis: verum

end;

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

hence x + 0 = x by Def2; :: thesis: verum

end;

end;