theorem :: CARD_2:27
for K being Cardinal holds
( exp (K,1) = K & exp (1,K) = 1 )