let A, B be Ordinal; :: thesis: (A *^ B) mod^ B = {}
A1: A *^ {} = {} by ORDINAL2:38;
A2: (A *^ B) -^ (A *^ B) = {} by Th67;
{} -^ (((A *^ B) div^ B) *^ B) = {} by Th69;
hence (A *^ B) mod^ B = {} by A1, A2, Th81; :: thesis: verum