for y, z being set
for F, Ch being Function st z in Intersection (F,Ch,y) & y in rng Ch holds
ex x being set st
( x in dom Ch & Ch . x = y & z in F . x )