theorem :: ORDINAL3:66

for A, B, C, D being Ordinal st A = (B *^ C) +^ D & D in C holds
( B = A div^ C & D = A mod^ C )