let k, n be natural Number ; :: thesis: (k * n) mod k = 0
A0: ( k is Nat & n is Nat ) by TARSKI:1;
per cases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; :: thesis: (k * n) mod k = 0
hence (k * n) mod k = 0 by Def2; :: thesis: verum
end;
suppose A1: k <> 0 ; :: thesis: (k * n) mod k = 0
k * n = (k * n) + 0 ;
hence (k * n) mod k = 0 by A0, A1, Def2; :: thesis: verum
end;
end;