theorem :: CARD_2:29

for K, M, N being Cardinal holds exp ((K *` M),N) = (exp (K,N)) *` (exp (M,N))