let N, M be Cardinal; :: thesis: Product (N --> M) = exp (M,N)
exp (M,N) = card (Funcs (N,M)) by CARD_3:def 3;
hence Product (N --> M) = exp (M,N) by CARD_3:11; :: thesis: verum