for x, y being set
for F, Ch being Function st not (dom F) /\ (Ch " {x}) is empty holds
( y in Intersection (F,Ch,x) iff for z being set st z in dom Ch & Ch . z = x holds
y in F . z )