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