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

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

suppose ( y is real & 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 y is real or not z is real ) ; :: thesis: x * (y + z) = (x * y) + (x * z)

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

end;

end;