let n, k, m be Nat; :: thesis: ( n divides k * m implies ex a, b being Nat st
( a divides k & b divides m & n = a * b ) )
assume A1: n divides k * m ; :: thesis: ex a, b being Nat st
( a divides k & b divides m & n = a * b )
take a = k gcd n; :: thesis: ex b being Nat st
( a divides k & b divides m & n = a * b )
A2: ( a divides k & a divides n ) by INT_2:def 2;

per cases ( a = 0 or a <> 0 ) ;

suppose A3: a = 0 ; :: thesis: ex b being Nat st
( a divides k & b divides m & n = a * b )

take m ; :: thesis: ( a divides k & m divides m & n = a * m )
thus ( a divides k & m divides m & n = a * m ) by A3; :: thesis: verum

end;

suppose A3: a <> 0 ; :: thesis: ex b being Nat st
( a divides k & b divides m & n = a * b )

consider b being Nat such that
A4: n = a * b by A2, NAT_D:def 3;
take b ; :: thesis: ( a divides k & b divides m & n = a * b )
A7: n divides m * n ;
a * m = |.m.| * a
.= (m * k) gcd (m * n) by INT_6:16 ;
then n divides a * m by A1, A7, INT_2:def 2;
hence ( a divides k & b divides m & n = a * b ) by A3, A4, INT_4:7, INT_2:def 2; :: thesis: verum

end;

end;