theorem Th5: :: LOPBAN_5:5

for X being RealBanachSpace
for Y being RealNormSpace
for T being Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( for x being Point of X ex K being Real st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x).|| <= K ) ) ) holds
ex L being Real st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= L ) )