let k, l, n be natural Number ; :: thesis: ( n <> 0 & k mod n = 0 & l < n implies (k + l) mod n = l )
A0: ( k is Nat & n is Nat & l is Nat ) by TARSKI:1;
assume that
A1: n <> 0 and
A2: k mod n = 0 and
A3: l < n ; :: thesis: (k + l) mod n = l
ex t being Nat st
( k = (n * t) + 0 & 0 < n ) by A1, A2, Def2;
hence (k + l) mod n = l by A0, A3, Def2; :: thesis: verum