theorem :: ARYTM_0:25

for x, y being Element of REAL holds opp (+ (x,y)) = + ((opp x),(opp y))