theorem Th3: :: LMOD_XX1:3

for M being AbGroup
for f, g being Endomorphism of M holds
( f in Funcs ( the carrier of M, the carrier of M) & g in Funcs ( the carrier of M, the carrier of M) & (add_End M) . [f,g] = (ADD (M,M)) . (f,g) & (ADD (M,M)) . (f,g) is Endomorphism of M )