let X, Y be RealNormSpace; :: thesis: 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 #)
let L be LinearOperator of X,Y; :: thesis: ( L is onto implies Im L = NORMSTR(# the carrier of Y, the ZeroF of Y, the addF of Y, the Mult of Y, the normF of Y #) )
assume L is onto ; :: thesis: Im L = NORMSTR(# the carrier of Y, the ZeroF of Y, the addF of Y, the Mult of Y, the normF of Y #)
then the carrier of (Im L) = the carrier of Y by LCL1, IMX2;
hence Im L = NORMSTR(# the carrier of Y, the ZeroF of Y, the addF of Y, the Mult of Y, the normF of Y #) by NSUBA; :: thesis: verum