let h, i, j be Integer; :: thesis: ( j is Multiple of i implies j + (h * i) is Multiple of i )
assume A1: i divides j ; :: according to NUMBER14:def 15 :: thesis: j + (h * i) is Multiple of i
i divides h * i ;
hence i divides j + (h * i) by A1, WSIERP_1:4; :: according to NUMBER14:def 15 :: thesis: verum