:: deftheorem defines Het RVSUM_3:def 5 :
for f being real-valued FinSequence holds Het f = card (HetSet f);