for X, Y, Z being RealNormSpace
for f being Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for g being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a, b being Real holds (a * b) * (f * g) = (a * f) * (b * g)