let x, y, z be ExtReal; :: thesis: ( y <= 0 & z <= 0 implies x * (y + z) = (x * y) + (x * z) )
assume A1: ( y <= 0 & z <= 0 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)
thus x * (y + z) = - (- (x * (y + z)))
.= - (x * (- (y + z))) by Th92
.= - (x * ((- y) + (- z))) by Th9
.= - ((x * (- y)) + (x * (- z))) by A1, Th96
.= - ((- (x * y)) + (x * (- z))) by Th92
.= - ((- (x * y)) + (- (x * z))) by Th92
.= - (- ((x * y) + (x * z))) by Th9
.= (x * y) + (x * z) ; :: thesis: verum