theorem Th45: :: CARD_FIN:46

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