let x, y, z be ExtReal; :: thesis: ( y = - z implies x * (y + z) = (x * y) + (x * z) )
assume A1: y = - z ; :: thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = x * 0 by Th7
.= (x * y) - (x * y) by Th7
.= (x * y) + (x * (- y)) by Th92
.= (x * y) + (x * z) by A1 ;
:: thesis: verum