for X being finite set
for k being Nat
for Fy being finite-yielding Function st dom Fy = X & k > card X holds
Card_Intersection (Fy,k) = 0