for F, Ch being Function
for x, y being object st x in Ch " {y} holds
(Intersection (F,(Ch | ((dom Ch) \ {x})),y)) /\ (F . x) = Intersection (F,Ch,y)