let F, Ch be Function; :: thesis: for x, y being object st x in Ch " {y} holds
(Intersection (F,(Ch | ((dom Ch) \ {x})),y)) /\ (F . x) = Intersection (F,Ch,y)
let x, y be object ; :: thesis: ( x in Ch " {y} implies (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);
assume x in Ch " {y} ; :: thesis: (Intersection (F,(Ch | ((dom Ch) \ {x})),y)) /\ (F . x) = Intersection (F,Ch,y)
then A1: Intersection (F,Ch,y) c= F . x by Th30;
A2: (Intersection (F,(Ch | ((dom Ch) \ {x})),y)) /\ (F . x) c= Intersection (F,Ch,y)

proof

let z be object ; :: 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 :: thesis: for x1 being set st x1 in dom Ch & Ch . x1 = y holds
z in F . x1

let x1 be set ; :: thesis: ( x1 in dom Ch & Ch . x1 = y implies z in F . b₁ )
assume that
A4: x1 in dom Ch and
A5: 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 A6: x1 in (dom Ch) \ {x} ; :: thesis: z in F . b₁

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

end;

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

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

end;

end;

end;

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

end;

Intersection (F,Ch,y) c= Intersection (F,(Ch | ((dom Ch) \ {x})),y) by Th26;
then Intersection (F,Ch,y) c= (Intersection (F,(Ch | ((dom Ch) \ {x})),y)) /\ (F . x) by A1, XBOOLE_1:19;
hence (Intersection (F,(Ch | ((dom Ch) \ {x})),y)) /\ (F . x) = Intersection (F,Ch,y) by A2; :: thesis: verum