for X being finite set
for Y being a_partition of X
for f being FinSequence of Y st f is one-to-one & rng f = Y holds
for c being FinSequence of NAT st len c = len f & ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) holds
card X = Sum c