theorem Th34: :: LOPBAN_1:34

for X, Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds
0 = ||.f.||