theorem Th1: :: PDIFF_9:1

for S, T being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (S,T))
for r being Real st 0 <= r & ( for x being Point of S st ||.x.|| <= 1 holds
||.(f . x).|| <= r * ||.x.|| ) holds
||.f.|| <= r