theorem :: CARD_FIN:42

for k being Nat
for Fy being finite-yielding Function st dom Fy is finite & k = 0 holds
Card_Intersection (Fy,k) = card (union (rng Fy))