let K, M, N be Cardinal; :: thesis: exp ((K *` M),N) = (exp (K,N)) *` (exp (M,N))
( card (K *` M) = K *` M & card N = card N ) ;
hence exp ((K *` M),N) = card (Funcs (N,[:K,M:])) by FUNCT_5:61
.= card [:(Funcs (N,K)),(Funcs (N,M)):] by FUNCT_5:64
.= (exp (K,N)) *` (exp (M,N)) by Th6 ;
:: thesis: verum