for R being Ring
for G being LeftMod of R holds
( dom (ID G) = G & cod (ID G) = G & ( for f being strict LModMorphism of R st cod f = G holds
(ID G) * f = f ) & ( for g being strict LModMorphism of R st dom g = G holds
g * (ID G) = g ) )