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

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 13;
b = a * d by A3;
hence b / a is Element of NAT by A1, XCMPLX_1:90; :: thesis: verum

end;

now

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:88;
hence a divides b by NAT_D:def 3; :: thesis: verum

end;

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