let i, j be Integer; :: thesis: i * j in multiples i
i * j is Multiple of i by Th57;
hence i * j in multiples i ; :: thesis: verum