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 Th9;
( {} *^ a = {} & {} *^ (n div^ m) = {} ) by ORDINAL2:52;
then {} <> m by A1, A2;
then ( {} in m & n = (a *^ m) +^ {} ) by A2, ORDINAL2:44, ORDINAL3:10;
hence contradiction by A1, A2, Def3, ORDINAL3:def 7; :: thesis: verum