let R be Ring; :: thesis: for V, W being LeftMod of R
for f being linear-transformation of V,W st f is onto holds
im f = (Omega). W
let V, W be LeftMod of R; :: thesis: for f being linear-transformation of V,W st f is onto holds
im f = (Omega). W
let f be linear-transformation of V,W; :: thesis: ( f is onto implies im f = (Omega). W )
assume f is onto ; :: thesis: im f = (Omega). W
then B1: rng f = the carrier of W by FUNCT_2:def 3;
B2: dom f = the carrier of V by FUNCT_2:def 1;
the carrier of (im f) = [#] (im f)
.= f .: ([#] V) by RANKNULL:def 2
.= the carrier of ((Omega). W) by B1, B2, RELAT_1:113 ;
hence im f = (Omega). W by VECTSP_4:29; :: thesis: verum