let n, m be natural Ordinal; :: thesis: ( m divides n iff n = m *^ (n div^ m) )
assume A1: ( ( m divides n & not n = m *^ (n div^ m) ) or ( n = m *^ (n div^ m) & not m divides n ) ) ; :: thesis: contradiction
then consider a being natural Ordinal such that
A2: n = m *^ a by Th5;
{} *^ a = {} by ORDINAL2:35;
then {} <> m by A1, A2, ORDINAL2:35;
then A3: {} in m by ORDINAL3:8;
n = (a *^ m) +^ {} by A2, ORDINAL2:27;
hence contradiction by A1, A2, A3, ORDINAL3:def 6; :: thesis: verum