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