A1: ( n = {} implies ( m div^ n = {} & {} *^ 1 = {} ) ) by ORDINAL2:35, ORDINAL3:def 6;
( n in 1 or 1 c= n ) by ORDINAL1:16;
then (m div^ n) *^ 1 c= (m div^ n) *^ n by A1, ORDINAL3:14, ORDINAL3:20;
then A2: m div^ n c= (m div^ n) *^ n by ORDINAL2:39;
( (m div^ n) *^ n c= m & m in omega ) by ORDINAL1:def 12, ORDINAL3:64;
hence m div^ n in omega by A2, ORDINAL1:12, XBOOLE_1:1; :: according to ORDINAL1:def 12 :: thesis: verum