theorem Th11: :: NDIFF13:10

for X, Y being RealNormSpace
for a being Real
for v1, v2 being Lipschitzian LinearOperator of X,Y
for w1, w2 being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st v1 = w1 & v2 = w2 holds
( v1 + v2 = w1 + w2 & a (#) v1 = a * w1 )