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