theorem Th29: :: CARD_FIN:30

for y, X9 being set
for F, Ch being Function st y in rng Ch & Ch " {y} c= X9 holds
Intersection ((F | X9),Ch,y) = Intersection (F,Ch,y)