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