theorem LOPBAN73: :: LOPBAN10:7

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