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:131;
[:M,{0 }:],M are_equipotent by Th13;
then A2: Funcs [:M,{0 }:],K, Funcs M,K are_equipotent by FUNCT_5:67;
[:N,{1}:],N are_equipotent by Th13;
then A3: Funcs [:N,{1}:],K, Funcs N,K are_equipotent by FUNCT_5:67;
M +` N,[:M,{0 }:] \/ [:N,{1}:] are_equipotent by Th17;
hence exp K,(M +` N) = card (Funcs ([:M,{0 }:] \/ [:N,{1}:]),K) by FUNCT_5:67
.= card [:(Funcs [:M,{0 }:],K),(Funcs [:N,{1}:],K):] by A1, FUNCT_5:69
.= card [:(Funcs M,K),(Funcs N,K):] by A2, A3, Th15
.= (exp K,M) *` (exp K,N) by Th14 ;
:: thesis: verum