for X being non empty finite set
for R being Equivalence_Relation of X
for S being Class b₂ -valued Function
for L being FinSequence of NAT st S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds
L . i = card (S . i) ) holds
card X = Sum L