theorem Th21:
for
R being
comRing for
M,
N being
LeftMod of
R for
f,
g being
Homomorphism of
R,
M,
N holds
(
f in Funcs ( the
carrier of
M, the
carrier of
N) &
g in Funcs ( the
carrier of
M, the
carrier of
N) &
(add_Hom (M,N)) . [f,g] = (ADD (M,N)) . (
f,
g) &
(ADD (M,N)) . (
f,
g) is
Homomorphism of
R,
M,
N )