for y being set
for F, Ch being Function st not Intersection (F,Ch,y) is empty holds
Ch " {y} c= dom F