let a, b be Nat; :: thesis: ( a <> 0 implies ( a divides b iff b / a is Element of NAT ) )
assume A1: a <> 0 ; :: thesis: ( a divides b iff b / a is Element of NAT )

A2: now :: thesis: ( a divides b implies b / a is Element of NAT )

assume a divides b ; :: thesis: b / a is Element of NAT
then consider d being Nat such that
A3: b = a * d by NAT_D:def 3;
reconsider d = d as Element of NAT by ORDINAL1:def 12;
b = a * d by A3;
hence b / a is Element of NAT by A1, XCMPLX_1:89; :: thesis: verum

end;

now :: thesis: ( b / a is Element of NAT implies a divides b )

assume b / a is Element of NAT ; :: thesis: a divides b
then reconsider d = b / a as Element of NAT ;
b = a * d by A1, XCMPLX_1:87;
hence a divides b ; :: thesis: verum

end;

hence ( a divides b iff b / a is Element of NAT ) by A2; :: thesis: verum