theorem Th52: :: CARD_FIN:53

for k being Nat
for Fy being finite-yielding Function
for X being finite set
for x being set
for n being Nat st dom Fy = X & x in dom Fy & k > 0 holds
Card_Intersection (Fy,(k + 1)) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),(k + 1))) + (Card_Intersection ((Intersect ((Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x)))),k))