theorem :: CARD_2:33

for K, M being Cardinal holds exp ((K +` M),2) = ((K *` K) +` ((2 *` K) *` M)) +` (M *` M)