let x1, x2, y be set ; :: thesis: for F, Ch being Function st {x1,x2} = Ch " {y} holds
Intersection (F,Ch,y) = (F . x1) /\ (F . x2)
let F, Ch 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:29;
hence Intersection (F,Ch,y) = (F . x1) /\ (F . x2) by A2, Th34; :: 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:132, XBOOLE_1:28, XBOOLE_1:49;
then (Ch " {y}) /\ ((dom Ch) \ {x1}) = {x2} by A3, ZFMISC_1:17;
then A4: (Ch | ((dom Ch) \ {x1})) " {y} = {x2} by FUNCT_1:70;
x1 in Ch " {y} by A1, TARSKI:def 2;
then (Intersection (F,(Ch | ((dom Ch) \ {x1})),y)) /\ (F . x1) = Intersection (F,Ch,y) by Th31;
hence Intersection (F,Ch,y) = (F . x1) /\ (F . x2) by A4, Th34; :: thesis: verum
end;
end;