:: deftheorem defines Im NORMSP_3:def 8 :
for X, Y being RealLinearSpace
for f being LinearOperator of X,Y holds Im f = Lin (rng f);