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

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

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

then ex a, b being Complex st
( x = a & 0 = b & x * 0 = a * b ) by Def5;
hence x * 0 = 0 ; :: thesis: verum

end;

suppose x = +infty ; :: thesis: x * 0 = 0

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

end;

suppose x = -infty ; :: thesis: x * 0 = 0

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

end;

end;