let x, y, z be ExtReal; :: thesis: ( x is real implies x * (y - z) = (x * y) - (x * z) )
assume x is real ; :: thesis: x * (y - z) = (x * y) - (x * z)
then x * (y - z) = (x * y) + (x * (- z)) by Th95
.= (x * y) + (- (x * z)) by Th92 ;
hence x * (y - z) = (x * y) - (x * z) ; :: thesis: verum