for X, Y being RealNormSpace
for L being LinearOperator of X,Y st L is onto holds
Im L = NORMSTR(# the carrier of Y, the ZeroF of Y, the addF of Y, the Mult of Y, the normF of Y #)