theorem Th31: :: CLOPBAN1:31

for X, Y being ComplexNormSpace
for f being Point of (C_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.||