theorem :: CARD_3:37

for K being Cardinal
for x being object holds Sum (x .--> K) = K