let A be Ordinal; :: thesis: ( A div^ 1 = A & A mod^ 1 = {} )
A1: A = A *^ 1 by ORDINAL2:39;
A2: A = A +^ {} by ORDINAL2:27;
A3: {} in 1 by Th10;
hence A div^ 1 = A by A1, A2, Def7; :: thesis: A mod^ 1 = {}
thus A mod^ 1 = A -^ A by A1, A2, A3, Def7
.= {} by Th67 ; :: thesis: verum