theorem :: LOPBAN13:6

for X being non trivial RealBanachSpace
for v1, v2 being Point of (R_NormSpace_of_BoundedLinearOperators (X,X))
for w1, w2 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X)
for a being Real st v1 = w1 & v2 = w2 holds
( v1 + v2 = w1 + w2 & a * v1 = a * w1 ) ;