let K, M, N be Cardinal; :: thesis: exp K,(M *` N) = exp (exp K,M),N
( [:M,N:],M *` N are_equipotent & [:N,M:],[:M,N:] are_equipotent ) by Lm2, CARD_1:def 5;
then A1: ( [:N,M:],M *` N are_equipotent & K,K are_equipotent ) by WELLORD2:22;
A2: ( Funcs M,K, card (Funcs M,K) are_equipotent & N,N are_equipotent ) by CARD_1:def 5;
thus exp K,(M *` N) = card (Funcs [:N,M:],K) by A1, FUNCT_5:67
.= card (Funcs N,(Funcs M,K)) by FUNCT_5:70
.= exp (exp K,M),N by A2, FUNCT_5:67 ; :: thesis: verum