let N, M be Cardinal; :: thesis: Product (N --> M) = exp M,N
set F = N --> M;
exp M,N = card (Funcs N,M) by CARD_2:def 3;
hence Product (N --> M) = exp M,N by Th20; :: thesis: verum