theorem Th47: :: CARD_FIN:48

for Fy being finite-yielding Function
for x being set st dom Fy is finite & x in dom Fy holds
Card_Intersection (Fy,1) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),1)) + (card (Fy . x))