for k being Nat
for n0, m0 being non zero Nat st n0,m0 are_coprime & k in NatDivisors (n0 * m0) holds
ex n1, m1 being Nat st
( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 )