let K be Cardinal; :: thesis: exp (K,0) = 1
thus exp (K,0) = card {{}} by FUNCT_5:57
.= 1 by CARD_1:30 ; :: thesis: verum