theorem Th32: :: LOPBAN_1:32

for X, Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for g being Lipschitzian LinearOperator of X,Y st g = f holds
for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||