theorem Th7: :: ARYTM_3:7

for n, m being natural Ordinal holds
( m divides n iff n = m *^ (n div^ m) )