Description: Sum of exponents law for ordinal exponentiation. Theorem 8R of Enderton p. 238. Also Proposition 8.41 of TakeutiZaring p. 69. (Contributed by Eric Schmidt, 26-May-2009)