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