:: deftheorem defines NKer NORMSP_3:def 7 :
for X, Y being RealNormSpace
for f being LinearOperator of X,Y holds NKer f = NLin (f " {(0. Y)});