let x, y be set ; :: thesis: for Ch, F being Function st x in Ch " {y} holds
(Intersection F,(Ch | ((dom Ch) \ {x})),y) /\ (F . x) = Intersection F,Ch,y
let Ch, F be Function; :: thesis: ( x in Ch " {y} implies (Intersection F,(Ch | ((dom Ch) \ {x})),y) /\ (F . x) = Intersection F,Ch,y )
assume A1: x in Ch " {y} ; :: thesis: (Intersection F,(Ch | ((dom Ch) \ {x})),y) /\ (F . x) = Intersection F,Ch,y
set d = (dom Ch) \ {x};
set Chd = Ch | ((dom Ch) \ {x});
set I1 = Intersection F,Ch,y;
set I2 = Intersection F,(Ch | ((dom Ch) \ {x})),y;
( Intersection F,Ch,y c= F . x & Intersection F,Ch,y c= Intersection F,(Ch | ((dom Ch) \ {x})),y ) by A1, Th29, Th33;
then A2: Intersection F,Ch,y c= (Intersection F,(Ch | ((dom Ch) \ {x})),y) /\ (F . x) by XBOOLE_1:19;
(Intersection F,(Ch | ((dom Ch) \ {x})),y) /\ (F . x) c= Intersection F,Ch,y

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in (Intersection F,(Ch | ((dom Ch) \ {x})),y) /\ (F . x) or z in Intersection F,Ch,y )
assume A3: z in (Intersection F,(Ch | ((dom Ch) \ {x})),y) /\ (F . x) ; :: thesis: z in Intersection F,Ch,y

now

let x1 be set ; :: thesis: ( x1 in dom Ch & Ch . x1 = y implies z in F . b₁ )
assume A4: ( x1 in dom Ch & Ch . x1 = y ) ; :: thesis: z in F . b₁

per cases ( x1 in (dom Ch) \ {x} or x1 in {x} ) by A4, XBOOLE_0:def 5;

suppose A5: x1 in (dom Ch) \ {x} ; :: thesis: z in F . b₁

( (dom Ch) /\ ((dom Ch) \ {x}) = dom (Ch | ((dom Ch) \ {x})) & (dom Ch) /\ ((dom Ch) \ {x}) = (dom Ch) \ {x} ) by RELAT_1:90, XBOOLE_1:28;
then ( x1 in dom (Ch | ((dom Ch) \ {x})) & (Ch | ((dom Ch) \ {x})) . x1 = y & z in Intersection F,(Ch | ((dom Ch) \ {x})),y ) by A3, A4, A5, FUNCT_1:70, XBOOLE_0:def 4;
hence z in F . x1 by Def2; :: thesis: verum

end;

suppose x1 in {x} ; :: thesis: z in F . b₁

then ( x1 = x & z in F . x ) by A3, TARSKI:def 1, XBOOLE_0:def 4;
hence z in F . x1 ; :: thesis: verum

end;

end;

end;

hence z in Intersection F,Ch,y by A3, Def2; :: thesis: verum

end;

hence (Intersection F,(Ch | ((dom Ch) \ {x})),y) /\ (F . x) = Intersection F,Ch,y by A2, XBOOLE_0:def 10; :: thesis: verum