let K be Cardinal; :: thesis: ( exp (K,1) = K & exp (1,K) = 1 )
thus exp (K,1) = card K by FUNCT_5:58, ORDINAL3:15
.= K ; :: thesis: exp (1,K) = 1
thus exp (1,K) = card {(K --> {})} by FUNCT_5:59, ORDINAL3:15
.= 1 by CARD_1:30 ; :: thesis: verum