let L be comRing; :: thesis: for n being Nat
for f, g being Element of L st f divides g holds
f divides n * g
let n be Nat; :: thesis: for f, g being Element of L st f divides g holds
f divides n * g
let f, g be Element of L; :: thesis: ( f divides g implies f divides n * g )
assume f divides g ; :: thesis: f divides n * g
then consider h being Element of L such that
A2: g = f * h by GCD_1:def 1;
n in NAT by ORDINAL1:def 12;
then n * g = f * (n * h) by A2, BINOM:19;
hence f divides n * g by GCD_1:def 1; :: thesis: verum