theorem :: CARD_2:32

for K being Cardinal holds exp (K,2) = K *` K by CARD_1:50, FUNCT_5:66;