theorem :: LOPBAN_8:2

for E, F, G being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (E,F))
for g being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) ex h being Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) st
( h = g * f & ||.h.|| <= ||.g.|| * ||.f.|| )