let K, M, N be Cardinal; :: thesis: exp (K,(M +` N)) = (exp (K,M)) *` (exp (K,N))
A1: [:M,{0}:] misses [:N,{1}:] by ZFMISC_1:108;
[:M,{0}:],M are_equipotent by CARD_1:69;
then A2: Funcs ([:M,{0}:],K), Funcs (M,K) are_equipotent by FUNCT_5:60;
[:N,{1}:],N are_equipotent by CARD_1:69;
then A3: Funcs ([:N,{1}:],K), Funcs (N,K) are_equipotent by FUNCT_5:60;
M +` N,[:M,{0}:] \/ [:N,{1}:] are_equipotent by Th9;
hence exp (K,(M +` N)) = card (Funcs (([:M,{0}:] \/ [:N,{1}:]),K)) by FUNCT_5:60
.= card [:(Funcs ([:M,{0}:],K)),(Funcs ([:N,{1}:],K)):] by A1, FUNCT_5:62
.= card [:(Funcs (M,K)),(Funcs (N,K)):] by A2, A3, Th7
.= (exp (K,M)) *` (exp (K,N)) by Th6 ;
:: thesis: verum