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