let A, B be Ordinal; :: thesis: ( B <> {} implies (A *^ B) div^ B = A )
assume B <> {} ; :: thesis: (A *^ B) div^ B = A
then A1: {} in B by Th8;
A *^ B = (A *^ B) +^ {} by ORDINAL2:27;
hence (A *^ B) div^ B = A by A1, Def6; :: thesis: verum