let F, Ch be Function; :: thesis: for x, y being object st {x} = Ch " {y} holds
Intersection (F,Ch,y) = F . x
let x, y be object ; :: 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:70;
then (Ch | ((dom Ch) \ {x})) " {y} = {} by A1;
then A3: Intersection (F,(Ch | ((dom Ch) \ {x})),y) = union (rng F) by Th33;
x in Ch " {y} by A2, TARSKI:def 1;
then A4: (union (rng F)) /\ (F . x) = Intersection (F,Ch,y) by A3, Th31;
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 3;
hence Intersection (F,Ch,y) = F . x by A4, XBOOLE_1:28, ZFMISC_1:74; :: thesis: verum
end;
suppose not x in dom F ; :: thesis: Intersection (F,Ch,y) = F . x
then F . x = {} by FUNCT_1:def 2;
hence Intersection (F,Ch,y) = F . x by A4; :: thesis: verum
end;
end;