:: deftheorem defines Im NORMSP_3:def 9 :
for X, Y being RealNormSpace
for f being LinearOperator of X,Y holds Im f = NLin (rng f);