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;
1 = succ 0
.= {0} ;
then A3: {} in 1 by Th8;
hence A div^ 1 = A by A1, A2, Def6; :: thesis: A mod^ 1 = {}
thus A mod^ 1 = A -^ A by A1, A2, A3, Def6
.= {} by Th54 ; :: thesis: verum