let i, j be Integer; :: thesis: i * j is Multiple of i
i divides i * j ;
hence i * j is Multiple of i by Def15; :: thesis: verum