let X9, y be set ; :: thesis: for F, Ch being Function holds Intersection (F | X9),Ch,y c= Intersection F,Ch,y
let F, Ch be Function; :: thesis: Intersection (F | X9),Ch,y c= Intersection F,Ch,y
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Intersection (F | X9),Ch,y or z in Intersection F,Ch,y )
assume A1: z in Intersection (F | X9),Ch,y ; :: thesis: z in Intersection F,Ch,y

A2: now

A3: Ch " {y} c= dom (F | X9) by A1, Th22;
let x be set ; :: thesis: ( x in dom Ch & Ch . x = y implies z in F . x )
assume that
A4: x in dom Ch and
A5: Ch . x = y ; :: thesis: z in F . x
Ch . x in {y} by A5, TARSKI:def 1;
then A6: x in Ch " {y} by A4, FUNCT_1:def 13;
z in (F | X9) . x by A1, A4, A5, Def2;
hence z in F . x by A6, A3, FUNCT_1:70; :: thesis: verum

end;

( union (rng (F | X9)) c= union (rng F) & z in union (rng (F | X9)) ) by A1, RELAT_1:99, ZFMISC_1:95;
hence z in Intersection F,Ch,y by A2, Def2; :: thesis: verum