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) st v1 = w1 & v2 = w2 holds
v1 * v2 = w1 * w2