let A, B, C, D be Ordinal; :: thesis: ( A = (B *^ C) +^ D & D in C implies ( B = A div^ C & D = A mod^ C ) )
assume that
A1: A = (B *^ C) +^ D and
A2: D in C ; :: thesis: ( B = A div^ C & D = A mod^ C )
thus B = A div^ C by A1, A2, Def6; :: thesis: D = A mod^ C
hence D = A mod^ C by A1, Th52; :: thesis: verum