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

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