theorem Th34: :: LOPBAN10:47

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