let R be Ring; :: thesis: for S being R -monomorphic Ring
for f being Monomorphism of R,S holds
( f " is one-to-one & f " is onto )
let S be R -monomorphic Ring; :: thesis: for f being Monomorphism of R,S holds
( f " is one-to-one & f " is onto )
let f be Monomorphism of R,S; :: thesis: ( f " is one-to-one & f " is onto )
rng (f ") = dom f by FUNCT_1:33
.= [#] R by FUNCT_2:def 1 ;
hence ( f " is one-to-one & f " is onto ) ; :: thesis: verum