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;