let K be Cardinal; :: thesis: ( exp (K,1) = K & exp (1,K) = 1 )
thus exp (K,1) = card K by FUNCT_5:65, ORDINAL3:18
.= K by CARD_1:def 5 ; :: thesis: exp (1,K) = 1
thus exp (1,K) = card {(K --> {})} by FUNCT_5:66, ORDINAL3:18
.= 1 by CARD_1:50 ; :: thesis: verum