theorem :: ANPROJ10:47

for V being RealLinearSpace
for x, y being Element of F_Real
for x9, y9 being Element of V st V = F_Real & x = x9 & y = y9 holds
x + y = x9 + y9 ;