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