let R be Ring; :: thesis: for M, N being LeftMod of R st M ~= N holds
N ~= M
let M, N be LeftMod of R; :: thesis: ( M ~= N implies N ~= M )
assume M ~= N ; :: thesis: N ~= M
then consider f being Homomorphism of R,M,N such that
A2: ( f is one-to-one & f is onto ) ;
reconsider g = f " as Function of N,M by A2, FUNCT_2:25;
A3: g is Homomorphism of R,N,M by A2, Th9;
g * f = id (dom f) by A2, FUNCT_1:39
.= id M by FUNCT_2:def 1 ;
then g is onto by FUNCT_2:23;
hence N ~= M by A3, A2; :: thesis: verum