let A, B be Ordinal; :: thesis: A = ((A div^ B) *^ B) +^ (A mod^ B)
(A div^ B) *^ B c= A by Th64;
hence A = ((A div^ B) *^ B) +^ (A mod^ B) by Def5; :: thesis: verum