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