((m div^ n) *^ n) +^ (m mod^ n) = m by ORDINAL3:65;
then A3: m mod^ n c= m by ORDINAL3:24;
m in omega by ORDINAL1:def 12;
hence m mod^ n in omega by A3, ORDINAL1:12; :: according to ORDINAL1:def 12 :: thesis: verum