theorem Th33: :: CLOPBAN1:33

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