let y, X9 be set ; :: thesis: for F, Ch being Function st y in rng Ch & Ch " {y} c= X9 holds
Intersection ((F | X9),Ch,y) = Intersection (F,Ch,y)
let F, Ch be Function; :: thesis: ( y in rng Ch & Ch " {y} c= X9 implies Intersection ((F | X9),Ch,y) = Intersection (F,Ch,y) )
assume that
A1: y in rng Ch and
A2: Ch " {y} c= X9 ; :: thesis: Intersection ((F | X9),Ch,y) = Intersection (F,Ch,y)
A3: Intersection (F,Ch,y) c= Intersection ((F | X9),Ch,y)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Intersection (F,Ch,y) or z in Intersection ((F | X9),Ch,y) )
assume A4: z in Intersection (F,Ch,y) ; :: thesis: z in Intersection ((F | X9),Ch,y)

A5: now :: thesis: for x being set st x in dom Ch & Ch . x = y holds
z in (F | X9) . x

let x be set ; :: thesis: ( x in dom Ch & Ch . x = y implies z in (F | X9) . x )
assume that
A6: x in dom Ch and
A7: Ch . x = y ; :: thesis: z in (F | X9) . x
Ch . x in {y} by A7, TARSKI:def 1;
then A8: x in Ch " {y} by A6, FUNCT_1:def 7;
z in F . x by A4, A6, A7, Def2;
then x in dom F by FUNCT_1:def 2;
then x in (dom F) /\ X9 by A2, A8, XBOOLE_0:def 4;
then A9: x in dom (F | X9) by RELAT_1:61;
z in F . x by A4, A6, A7, Def2;
hence z in (F | X9) . x by A9, FUNCT_1:47; :: thesis: verum

end;

consider x being set such that
A10: x in dom Ch and
A11: Ch . x = y and
A12: z in F . x by A1, A4, Th21;
Ch . x in {y} by A11, TARSKI:def 1;
then A13: x in Ch " {y} by A10, FUNCT_1:def 7;
x in dom F by A12, FUNCT_1:def 2;
then x in (dom F) /\ X9 by A2, A13, XBOOLE_0:def 4;
then x in dom (F | X9) by RELAT_1:61;
then A14: (F | X9) . x in rng (F | X9) by FUNCT_1:def 3;
z in (F | X9) . x by A5, A10, A11;
then z in union (rng (F | X9)) by A14, TARSKI:def 4;
hence z in Intersection ((F | X9),Ch,y) by A5, Def2; :: thesis: verum

end;

Intersection ((F | X9),Ch,y) c= Intersection (F,Ch,y) by Th28;
hence Intersection ((F | X9),Ch,y) = Intersection (F,Ch,y) by A3; :: thesis: verum