A1: ( n = {} implies ( m div^ n = {} & {} *^ 1 = {} ) ) by ORDINAL2:52, ORDINAL3:def 7;
( n in 1 or 1 c= n ) by ORDINAL1:26;
then (m div^ n) *^ 1 c= (m div^ n) *^ n by A1, ORDINAL3:17, ORDINAL3:23;
then A2: m div^ n c= (m div^ n) *^ n by ORDINAL2:56;
( (m div^ n) *^ n c= m & m in omega ) by ORDINAL1:def 13, ORDINAL3:77;
hence m div^ n in omega by A2, ORDINAL1:22, XBOOLE_1:1; :: according to ORDINAL1:def 13 :: thesis: verum