let x, y be set ; :: thesis: for F, Ch being Function st not (dom F) /\ (Ch " {x}) is empty holds
( y in Intersection (F,Ch,x) iff for z being set st z in dom Ch & Ch . z = x holds
y in F . z )
let F, Ch be Function; :: thesis: ( not (dom F) /\ (Ch " {x}) is empty implies ( y in Intersection (F,Ch,x) iff for z being set st z in dom Ch & Ch . z = x holds
y in F . z ) )
assume A1: not (dom F) /\ (Ch " {x}) is empty ; :: thesis: ( y in Intersection (F,Ch,x) iff for z being set st z in dom Ch & Ch . z = x holds
y in F . z )
thus ( y in Intersection (F,Ch,x) implies for z being set st z in dom Ch & Ch . z = x holds
y in F . z ) by Def2; :: thesis: ( ( for z being set st z in dom Ch & Ch . z = x holds
y in F . z ) implies y in Intersection (F,Ch,x) )
thus ( ( for z being set st z in dom Ch & Ch . z = x holds
y in F . z ) implies y in Intersection (F,Ch,x) ) :: thesis: verum

proof

consider z being object such that
A2: z in (dom F) /\ (Ch " {x}) by A1;
A3: z in Ch " {x} by A2, XBOOLE_0:def 4;
then Ch . z in {x} by FUNCT_1:def 7;
then A4: Ch . z = x by TARSKI:def 1;
z in dom F by A2, XBOOLE_0:def 4;
then A5: F . z in rng F by FUNCT_1:def 3;
assume A6: for z being set st z in dom Ch & Ch . z = x holds
y in F . z ; :: thesis: y in Intersection (F,Ch,x)
z in dom Ch by A3, FUNCT_1:def 7;
then y in F . z by A6, A4;
then y in union (rng F) by A5, TARSKI:def 4;
hence y in Intersection (F,Ch,x) by A6, Def2; :: thesis: verum

end;