theorem Th61: :: PRE_POLY:63

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)))