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