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

end;

end;