let b, a be Nat; :: thesis: for k being Integer st b <> 0 & a * k = b holds
k is Element of NAT
let k be Integer; :: thesis: ( b <> 0 & a * k = b implies k is Element of NAT )
assume A1: ( b <> 0 & a * k = b ) ; :: thesis: k is Element of NAT
then A2: a divides b by INT_1:def 9;
A3: a <> 0 by A1;
then k = b / a by A1, XCMPLX_1:90;
hence k is Element of NAT by A2, A3, Lm5; :: thesis: verum