for M, N being Cardinal holds Product (N --> M) = exp (M,N) by CARD_3:11;