let A be Ordinal; :: thesis: ( {} div^ A = {} & {} mod^ A = {} & A mod^ {} = A )
A1: ( A = {} or A <> {} ) ;
{} = {} *^ A by ORDINAL2:35;
hence {} div^ A = {} by A1, Def6, Th68; :: thesis: ( {} mod^ A = {} & A mod^ {} = A )
thus {} mod^ A = {} by Th56; :: thesis: A mod^ {} = A
thus A mod^ {} = A -^ {} by ORDINAL2:38
.= A by Th56 ; :: thesis: verum