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