let K be Cardinal; :: thesis: exp K,0 = 1
thus exp K,0 = card {{} } by FUNCT_5:64
.= 1 by CARD_1:50 ; :: thesis: verum