theorem Th37: :: LOPBAN_9:21

for X, Y, Z being RealNormSpace
for f, g being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))
for a being Real holds
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ) & ( f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )