let x, y, z be ExtReal; :: thesis: ( x is real & not y is real implies x * (y + z) = (x * y) + (x * z) )
assume that
A1: x is real and
A2: not y is real ; :: thesis: x * (y + z) = (x * y) + (x * z)

per cases ( z is real or not z is real ) ;

suppose z is real ; :: thesis: x * (y + z) = (x * y) + (x * z)

hence x * (y + z) = (x * y) + (x * z) by A1, Lm27; :: thesis: verum

end;

suppose not z is real ; :: thesis: x * (y + z) = (x * y) + (x * z)

then A3: not z in REAL ;
A4: not y in REAL by A2;

per cases ( ( y = -infty & z = -infty ) or ( y = -infty & z = +infty ) or ( y = +infty & z = -infty ) or ( y = +infty & z = +infty ) ) by A4, A3, XXREAL_0:14;

suppose ( y = -infty & z = -infty ) ; :: thesis: x * (y + z) = (x * y) + (x * z)

hence x * (y + z) = (x * y) + (x * z) by Lm24; :: thesis: verum

end;

suppose ( y = -infty & z = +infty ) ; :: thesis: x * (y + z) = (x * y) + (x * z)

hence x * (y + z) = (x * y) + (x * z) by Th5, Th93; :: thesis: verum

end;

suppose ( y = +infty & z = -infty ) ; :: thesis: x * (y + z) = (x * y) + (x * z)

hence x * (y + z) = (x * y) + (x * z) by Th6, Th93; :: thesis: verum

end;

suppose ( y = +infty & z = +infty ) ; :: thesis: x * (y + z) = (x * y) + (x * z)

hence x * (y + z) = (x * y) + (x * z) by Lm24; :: thesis: verum

end;

end;

end;

end;