theorem Th27: :: CARD_FIN:28

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