theorem Lm2: :: E_TRANS1:7

for L being comRing
for n being Nat
for f, g being Element of L st f divides g holds
f divides n * g