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