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

proof

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

now :: thesis: for x being set st x in dom Ch & Ch . x = y holds
z in F . x

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 | X9) " {y} by A1, A4, FUNCT_1:def 7;
then (Ch | X9) . x in {y} by FUNCT_1:def 7;
then A7: (Ch | X9) . x = y by TARSKI:def 1;
x in dom (Ch | X9) by A6, FUNCT_1:def 7;
hence z in F . x by A3, A7, Def2; :: thesis: verum

end;

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

end;

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