((m div^ n) *^ n) +^ (m mod^ n) = m by ORDINAL3:78;
then A3: m mod^ n c= m by ORDINAL3:27;
m in omega by ORDINAL1:def 13;
hence m mod^ n in omega by A3, ORDINAL1:22; :: according to ORDINAL1:def 13 :: thesis: verum