for y, X9 being set
for F, Ch being Function holds (Intersection (F,Ch,y)) /\ X9 = Intersection ((Intersect (F,((dom F) --> X9))),Ch,y)