let R be Ring; :: thesis: 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
let M, N be LeftMod of R; :: thesis: 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
let f be Homomorphism of R,M,N; :: thesis: ( f is one-to-one & f is onto implies f " is Homomorphism of R,N,M )
assume A1: ( f is one-to-one & f is onto ) ; :: thesis: f " is Homomorphism of R,N,M
reconsider g = f " as Function of N,M by A1, FUNCT_2:25;
for a, b being Element of the carrier of N holds g . (a + b) = (g . a) + (g . b)

proof

let a, b be Element of N; :: thesis: g . (a + b) = (g . a) + (g . b)
consider x being object such that
A2: ( x in the carrier of M & a = f . x ) by A1, FUNCT_2:11;
reconsider x = x as Element of M by A2;
consider y being object such that
A3: ( y in the carrier of M & b = f . y ) by A1, FUNCT_2:11;
reconsider y = y as Element of M by A3;
(g . a) + (g . b) = x + (g . (f . y)) by A1, A2, A3, FUNCT_2:26
.= x + y by A1, FUNCT_2:26
.= g . (f . (x + y)) by A1, FUNCT_2:26
.= g . (a + b) by A2, A3, VECTSP_1:def 20, Def10 ;
hence g . (a + b) = (g . a) + (g . b) ; :: thesis: verum

end;

then A4: g is additive ;
for r being Element of R
for a being Element of the carrier of N holds g . (r * a) = r * (g . a)

proof

let r be Element of R; :: thesis: for a being Element of the carrier of N holds g . (r * a) = r * (g . a)
let a be Element of the carrier of N; :: thesis: g . (r * a) = r * (g . a)
consider x being object such that
A5: ( x in the carrier of M & a = f . x ) by A1, FUNCT_2:11;
reconsider x = x as Element of M by A5;
g . (r * a) = g . (f . (r * x)) by A5, MOD_2:def 2, Def10
.= r * x by A1, FUNCT_2:26
.= r * (g . a) by A1, A5, FUNCT_2:26 ;
hence g . (r * a) = r * (g . a) ; :: thesis: verum

end;

then g is homogeneous ;
hence f " is Homomorphism of R,N,M by A4, Def10; :: thesis: verum