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 A1: ( A = (B *^ C) +^ D & D in C ) ; :: thesis: ( B = A div^ C & D = A mod^ C )
hence B = A div^ C by Def7; :: thesis: D = A mod^ C
hence D = A mod^ C by A1, Th65; :: thesis: verum