for n being Nat
for k, m, m1, n1 being Element of NAT st k divides m & k divides n holds
k divides (m * m1) + (n * n1)