let h, i, j be natural Number ; :: thesis: ( i divides j & i divides h implies i divides j + h )
assume that
A1: i divides j and
A2: i divides h ; :: thesis: i divides j + h
A3: j = i * (j div i) by A1, Th3;
h = i * (h div i) by A2, Th3;
then j + h = i * ((j div i) + (h div i)) by A3;
hence i divides j + h ; :: thesis: verum