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