let R be comRing; :: thesis: for M being LeftMod of R holds
( rho M is one-to-one & rho M is onto )
let M be LeftMod of R; :: thesis: ( rho M is one-to-one & rho M is onto )
reconsider EM = AbGrLMod ((AbGr M),(canHom M)) as LeftMod of R ;
set f = rho M;
for y being object st y in the carrier of EM holds
ex x being object st
( x in the carrier of M & y = (rho M) . x )

proof

let y be object ; :: thesis: ( y in the carrier of EM implies ex x being object st
( x in the carrier of M & y = (rho M) . x ) )
assume y in the carrier of EM ; :: thesis: ex x being object st
( x in the carrier of M & y = (rho M) . x )
then consider x being object such that
A6: ( x = y & x in the carrier of M ) ;
reconsider x0 = x as Element of the carrier of M by A6;
(rho M) . x0 = x0 ;
hence ex x being object st
( x in the carrier of M & y = (rho M) . x ) by A6; :: thesis: verum

end;

hence ( rho M is one-to-one & rho M is onto ) by FUNCT_2:10; :: thesis: verum