let m, n be natural Ordinal; :: thesis: ( n <> {} implies (m *^ n) div^ (m lcm n) divides m )
assume A1: n <> {} ; :: thesis: (m *^ n) div^ (m lcm n) divides m
take (m lcm n) div^ n ; :: according to ARYTM_3:def 3 :: thesis: m = ((m *^ n) div^ (m lcm n)) *^ ((m lcm n) div^ n)
n divides m lcm n by Def4;
then A2: m lcm n = n *^ ((m lcm n) div^ n) by Th7;
m lcm n divides m *^ n by Th12;
then m *^ n = (m lcm n) *^ ((m *^ n) div^ (m lcm n)) by Th7;
then n *^ m = n *^ (((m lcm n) div^ n) *^ ((m *^ n) div^ (m lcm n))) by A2, ORDINAL3:50;
hence m = ((m *^ n) div^ (m lcm n)) *^ ((m lcm n) div^ n) by A1, ORDINAL3:33; :: thesis: verum