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