let i1, i2 be Integer; :: thesis: for n being Nat st n > 0 & i1 mod n = 0 holds
(i1 * i2) mod n = 0
let n be Nat; :: thesis: ( n > 0 & i1 mod n = 0 implies (i1 * i2) mod n = 0 )
assume that
A1: n > 0 and
A2: i1 mod n = 0 ; :: thesis: (i1 * i2) mod n = 0
n divides i1 by A1, A2, INT_1:62;
then n divides i1 * i2 by INT_2:2;
hence (i1 * i2) mod n = 0 by A1, INT_1:62; :: thesis: verum