let z, y be set ; :: thesis: 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 )
let F, Ch be Function; :: thesis: ( z in Intersection F,Ch,y & y in rng Ch implies ex x being set st
( x in dom Ch & Ch . x = y & z in F . x ) )
assume A1: ( z in Intersection F,Ch,y & y in rng Ch ) ; :: thesis: ex x being set st
( x in dom Ch & Ch . x = y & z in F . x )
then Ch " {y} <> {} by FUNCT_1:142;
then consider x being set such that
A2: x in Ch " {y} by XBOOLE_0:def 1;
Ch . x in {y} by A2, FUNCT_1:def 13;
then ( Ch . x = y & x in dom Ch ) by A2, FUNCT_1:def 13, TARSKI:def 1;
then ( x in dom Ch & Ch . x = y & z in F . x ) by A1, Def2;
hence ex x being set st
( x in dom Ch & Ch . x = y & z in F . x ) ; :: thesis: verum