for Fy being finite-yielding Function
for X being finite set st dom Fy = X holds
for P being Function of (card X),X st P is one-to-one holds
ex XFS being XFinSequence of NAT st
( dom XFS = card X & ( for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) ) & Card_Intersection (Fy,1) = Sum XFS )