let k, m, n be Nat; :: thesis: ( n divides m & k divides m & n,k are_coprime implies n * k divides m )
assume that
A1: n divides m and
A2: ( k divides m & n,k are_coprime ) ; :: thesis: n * k divides m
consider t1 being Nat such that
A3: m = n * t1 by A1, NAT_D:def 3;
k divides t1 by A2, A3, Th3;
then consider t2 being Nat such that
A4: t1 = k * t2 by NAT_D:def 3;
m = (n * k) * t2 by A3, A4;
hence n * k divides m ; :: thesis: verum