let A be Ordinal; :: thesis: ( {} div^ A = {} & {} mod^ A = {} & A mod^ {} = A )
( {} = {} *^ A & ( A = {} or A <> {} ) ) by ORDINAL2:52;
hence {} div^ A = {} by Def7, Th81; :: thesis: ( {} mod^ A = {} & A mod^ {} = A )
thus {} mod^ A = {} by Th69; :: thesis: A mod^ {} = A
thus A mod^ {} = A -^ {} by ORDINAL2:55
.= A by Th69 ; :: thesis: verum