for n, m being Nat
for f1, f2 being Function of (REAL m),(REAL n)
for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2