let x, y, z be ext-real number ; :: 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 Th106
.= (x * y) + (- (x * z)) by Th103 ;
hence x * (y - z) = (x * y) - (x * z) ; :: thesis: verum