let A, B be Ordinal; :: thesis: A = ((A div^ B) *^ B) +^ (A mod^ B)
( (A div^ B) *^ B c= A & A mod^ B = A -^ ((A div^ B) *^ B) ) by Th77;
hence A = ((A div^ B) *^ B) +^ (A mod^ B) by Def6; :: thesis: verum