let R be Ring; :: thesis: for L, M, N being LeftMod of R st L ~= M & M ~= N holds
L ~= N
let L, M, N be LeftMod of R; :: thesis: ( L ~= M & M ~= N implies L ~= N )
assume A1: ( L ~= M & M ~= N ) ; :: thesis: L ~= N
then consider f being Homomorphism of R,L,M such that
A2: ( f is one-to-one & f is onto ) ;
consider g being Homomorphism of R,M,N such that
A3: ( g is one-to-one & g is onto ) by A1;
reconsider G = g * f as Function of L,N ;
for x, y being Element of L holds G . (x + y) = (G . x) + (G . y)

proof

let x, y be Element of L; :: thesis: G . (x + y) = (G . x) + (G . y)
A4: G . x = g . (f . x) by FUNCT_2:15;
A5: G . y = g . (f . y) by FUNCT_2:15;
G . (x + y) = g . (f . (x + y)) by FUNCT_2:15
.= g . ((f . x) + (f . y)) by Def10, VECTSP_1:def 20
.= (G . x) + (G . y) by A4, A5, Def10, VECTSP_1:def 20 ;
hence G . (x + y) = (G . x) + (G . y) ; :: thesis: verum

end;

then A6: G is additive ;
for x being Element of L
for a being Element of R holds G . (a * x) = a * (G . x)

proof

let x be Element of L; :: thesis: for a being Element of R holds G . (a * x) = a * (G . x)
let a be Element of R; :: thesis: G . (a * x) = a * (G . x)
A7: G . x = g . (f . x) by FUNCT_2:15;
G . (a * x) = g . (f . (a * x)) by FUNCT_2:15
.= g . (a * (f . x)) by Def10, MOD_2:def 2
.= a * (G . x) by A7, Def10, MOD_2:def 2 ;
hence G . (a * x) = a * (G . x) ; :: thesis: verum

end;

then G is homogeneous ;
then A8: G is Homomorphism of R,L,N by A6, Def10;
( G is one-to-one & G is onto ) by A2, A3, FUNCT_2:27;
hence L ~= N by A8; :: thesis: verum