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