let x, y be Element of REAL ; :: thesis: * ((opp x),y) = opp (* (x,y))
+ ((* ((opp x),y)),(* (x,y))) = * ((+ ((opp x),x)),y) by Th14
.= 0 by Th12, Def3 ;
hence * ((opp x),y) = opp (* (x,y)) by Def3; :: thesis: verum