theorem Th32: :: LOPBAN_9:16

for X, Y, Z being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))
for g being Lipschitzian BilinearOperator of X,Y,Z st g = f holds
for t being VECTOR of X
for s being VECTOR of Y holds ||.(g . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.||