let B, A be Ordinal; :: thesis: ( B <> {} implies (A *^ B) div^ B = A )
assume B <> {} ; :: thesis: (A *^ B) div^ B = A
then ( {} in B & A *^ B = (A *^ B) +^ {} ) by Th10, ORDINAL2:44;
hence (A *^ B) div^ B = A by Def7; :: thesis: verum