theorem :: CARD_FIN:38

for y being set
for Ch being Function
for Fy being finite-yielding Function st y in rng Ch holds
Intersection (Fy,Ch,y) is finite