for X being finite set
for Fy being finite-yielding Function
for x being object st dom Fy = X holds
Card_Intersection (Fy,(card X)) = card (Intersection (Fy,(X --> x),x))