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 )
A1: (dom Ch) \ {x} misses {x} by XBOOLE_1:79;
assume A2: {x} = Ch " {y} ; :: thesis: Intersection (F,Ch,y) = F . x
then (Ch | ((dom Ch) \ {x})) " {y} = ((dom Ch) \ {x}) /\ {x} by FUNCT_1:139;
then (Ch | ((dom Ch) \ {x})) " {y} = {} by A1, XBOOLE_0:def 7;
then A3: Intersection (F,(Ch | ((dom Ch) \ {x})),y) = union (rng F) by Th36;
x in Ch " {y} by A2, TARSKI:def 1;
then A4: (union (rng F)) /\ (F . x) = Intersection (F,Ch,y) by A3, 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 A4, 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 A4; :: thesis: verum

end;

end;