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

proof

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

A5: now

let x be set ; :: thesis: ( x in dom Ch & Ch . x = y implies z in (F | X') . x )
assume that
A6: x in dom Ch and
A7: Ch . x = y ; :: thesis: z in (F | X') . x
Ch . x in {y} by A7, TARSKI:def 1;
then A8: x in Ch " {y} by A6, FUNCT_1:def 13;
z in F . x by A4, A6, A7, Def2;
then x in dom F by FUNCT_1:def 4;
then x in (dom F) /\ X' by A2, A8, XBOOLE_0:def 4;
then A9: x in dom (F | X') by RELAT_1:90;
z in F . x by A4, A6, A7, Def2;
hence z in (F | X') . x by A9, FUNCT_1:70; :: 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, Th24;
Ch . x in {y} by A11, TARSKI:def 1;
then A13: x in Ch " {y} by A10, FUNCT_1:def 13;
x in dom F by A12, FUNCT_1:def 4;
then x in (dom F) /\ X' by A2, A13, XBOOLE_0:def 4;
then x in dom (F | X') by RELAT_1:90;
then A14: (F | X') . x in rng (F | X') by FUNCT_1:def 5;
z in (F | X') . x by A5, A10, A11;
then z in union (rng (F | X')) by A14, TARSKI:def 4;
hence z in Intersection (F | X'),Ch,y by A5, Def2; :: thesis: verum

end;

Intersection (F | X'),Ch,y c= Intersection F,Ch,y by Th31;
hence Intersection (F | X'),Ch,y = Intersection F,Ch,y by A3, XBOOLE_0:def 10; :: thesis: verum