for X, Y, Z being RealNormSpace
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Z)) st w = v * u holds
||.w.|| <= ||.v.|| * ||.u.||