let n, k, p be Integer; :: thesis: ( p divides k implies ( n in multiples p iff n + k in multiples p ) )
assume A1: p divides k ; :: thesis: ( n in multiples p iff n + k in multiples p )
thus ( n in multiples p implies n + k in multiples p ) :: thesis: ( n + k in multiples p implies n in multiples p )

proof

assume n in multiples p ; :: thesis: n + k in multiples p
then p divides n by NUMBER14:62;
hence n + k in multiples p by NUMBER14:62, A1, WSIERP_1:4; :: thesis: verum

end;

assume n + k in multiples p ; :: thesis: n in multiples p
then p divides n + k by NUMBER14:62;
hence n in multiples p by NUMBER14:62, A1, INT_2:1; :: thesis: verum