let x1, x2, y be set ; :: thesis: for Ch, F being Function st {x1,x2} = Ch " {y} holds
Intersection (F,Ch,y) = (F . x1) /\ (F . x2)
let Ch, F be Function; :: thesis: ( {x1,x2} = Ch " {y} implies Intersection (F,Ch,y) = (F . x1) /\ (F . x2) )
assume A1: {x1,x2} = Ch " {y} ; :: thesis: Intersection (F,Ch,y) = (F . x1) /\ (F . x2)

per cases ( x1 = x2 or x1 <> x2 ) ;

suppose A2: x1 = x2 ; :: thesis: Intersection (F,Ch,y) = (F . x1) /\ (F . x2)

then Ch " {y} = {x1} by A1, ENUMSET1:69;
hence Intersection (F,Ch,y) = (F . x1) /\ (F . x2) by A2, Th37; :: thesis: verum

end;

suppose A3: x1 <> x2 ; :: thesis: Intersection (F,Ch,y) = (F . x1) /\ (F . x2)

( (Ch " {y}) /\ ((dom Ch) \ {x1}) = ((Ch " {y}) /\ (dom Ch)) \ {x1} & (Ch " {y}) /\ (dom Ch) = {x1,x2} ) by A1, RELAT_1:167, XBOOLE_1:28, XBOOLE_1:49;
then (Ch " {y}) /\ ((dom Ch) \ {x1}) = {x2} by A3, ZFMISC_1:23;
then A4: (Ch | ((dom Ch) \ {x1})) " {y} = {x2} by FUNCT_1:139;
x1 in Ch " {y} by A1, TARSKI:def 2;
then (Intersection (F,(Ch | ((dom Ch) \ {x1})),y)) /\ (F . x1) = Intersection (F,Ch,y) by Th34;
hence Intersection (F,Ch,y) = (F . x1) /\ (F . x2) by A4, Th37; :: thesis: verum

end;

end;