theorem Th9: :: LMOD_XX1:9
for R being Ring
for M, N being LeftMod of R
for f being Homomorphism of R,M,N st f is one-to-one & f is onto holds
f " is Homomorphism of R,N,M