let x, y be ext-real number ; :: thesis: - (x * y) = (- x) * y
thus - (x * y) = (- 1) * (x * y) by Th7
.= ((- 1) * x) * y by Th6
.= (- x) * y by Th7 ; :: thesis: verum