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