for X being non empty set
for f being finite-support Function of X,NAT holds card (NatMinor f) = multnat $$ ((support f),(addnat [:] (f,1)))