let x, y, z be ext-real number ; :: thesis: ( x is real implies x * (y + z) = (x * y) + (x * z) )
assume Z: 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 Z, Lm12A; :: 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 Z, Lm12B; :: thesis: verum

end;

end;