let x, y be set ; :: thesis: for Ch, F being Function st {x} = Ch " {y} holds
Intersection F,Ch,y = F . x
let Ch, F be Function; :: thesis: ( {x} = Ch " {y} implies Intersection F,Ch,y = F . x )
assume A1: {x} = Ch " {y} ; :: thesis: Intersection F,Ch,y = F . x
then ( (Ch | ((dom Ch) \ {x})) " {y} = ((dom Ch) \ {x}) /\ {x} & (dom Ch) \ {x} misses {x} ) by FUNCT_1:139, XBOOLE_1:79;
then (Ch | ((dom Ch) \ {x})) " {y} = {} by XBOOLE_0:def 7;
then ( Intersection F,(Ch | ((dom Ch) \ {x})),y = union (rng F) & x in Ch " {y} ) by A1, Th36, TARSKI:def 1;
then A2: (union (rng F)) /\ (F . x) = Intersection F,Ch,y by Th34;

per cases ( x in dom F or not x in dom F ) ;

suppose x in dom F ; :: thesis: Intersection F,Ch,y = F . x

then F . x in rng F by FUNCT_1:def 5;
hence Intersection F,Ch,y = F . x by A2, XBOOLE_1:28, ZFMISC_1:92; :: thesis: verum

end;

suppose not x in dom F ; :: thesis: Intersection F,Ch,y = F . x

then F . x = {} by FUNCT_1:def 4;
hence Intersection F,Ch,y = F . x by A2; :: thesis: verum

end;

end;