let k, m, n be Integer; :: thesis: ( k divides m & k divides n implies k divides m + n )
assume that
A1: k divides m and
A2: k divides n ; :: thesis: k divides m + n
consider m1 being Integer such that
A3: m = k * m1 by A1;
consider n1 being Integer such that
A4: n = k * n1 by A2;
m + n = k * (m1 + n1) by A3, A4;
hence k divides m + n ; :: thesis: verum