for x, y being set
for F being Function st not F is empty holds
( y in Intersection (F,((dom F) --> x),x) iff for z being set st z in dom F holds
y in F . z )