let A, B be Ordinal; :: thesis: (A *^ B) mod^ B = {}
( A *^ {} = {} & {} div^ {} = {} & (A *^ B) mod^ B = (A *^ B) -^ (((A *^ B) div^ B) *^ B) & {} -^ (((A *^ B) div^ B) *^ B) = {} & ( B = {} or B <> {} ) & (A *^ B) -^ (A *^ B) = {} ) by Def7, Th67, Th69, ORDINAL2:55;
hence (A *^ B) mod^ B = {} by Th81; :: thesis: verum