let n be Nat; :: thesis: for k, m, m1, n1 being Element of NAT st k divides m & k divides n holds
k divides (m * m1) + (n * n1)
let k, m, m1, n1 be Element of NAT ; :: thesis: ( k divides m & k divides n implies k divides (m * m1) + (n * n1) )
assume ( k divides m & k divides n ) ; :: thesis: k divides (m * m1) + (n * n1)
then ( k divides m * m1 & k divides n * n1 ) by NAT_D:9;
hence k divides (m * m1) + (n * n1) by NAT_D:8; :: thesis: verum