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 A1: ( n > 0 & i1 mod n = 0 ) ; :: thesis: (i1 * i2) mod n = 0
then n divides i1 by INT_1:89;
then n divides i1 * i2 by INT_2:12;
hence (i1 * i2) mod n = 0 by A1, INT_1:89; :: thesis: verum