let y, z, x be ext-real number ; :: thesis: ( y <= 0 & z <= 0 implies x * (y + z) = (x * y) + (x * z) )
assume Z: ( y <= 0 & z <= 0 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)
thus x * (y + z) = - (- (x * (y + z)))
.= - (x * (- (y + z))) by Th8o
.= - (x * ((- y) + (- z))) by Th9
.= - ((x * (- y)) + (x * (- z))) by Z, Th14
.= - ((- (x * y)) + (x * (- z))) by Th8o
.= - ((- (x * y)) + (- (x * z))) by Th8o
.= - (- ((x * y) + (x * z))) by Th9
.= (x * y) + (x * z) ; :: thesis: verum