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