for X being non trivial RealBanachSpace
for v1, v2 being Lipschitzian LinearOperator of 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 & v1 + v2 = w1 + w2 & a (#) v1 = a * w1 )