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:68
.= card [:(Funcs N,K),(Funcs N,M):] by FUNCT_5:71
.= (exp K,N) *` (exp M,N) by Th14 ;
:: thesis: verum