:: deftheorem defines exp CARD_2:def 3 :
for M, N being Cardinal holds exp (M,N) = card (Funcs (N,M));