theorem Th65: :: ORDINAL3:65

for A, B being Ordinal holds A = ((A div^ B) *^ B) +^ (A mod^ B)