theorem Th3: :: LOPBAN_7:3

for X, Y being RealNormSpace
for f being LinearOperator of X,Y holds 0. Y = f . (0. X)