let i, j, z be Integer; :: thesis: ( j <> 0 & z = i / j implies z divides i )
assume A1: ( j <> 0 & z = i / j ) ; :: thesis: z divides i
take j ; :: according to INT_1:def 3 :: thesis: i = z * j
thus i = z * j by A1, XCMPLX_1:87; :: thesis: verum