let y, X9 be set ; :: thesis: for Ch, F being Function st Ch " {y} = (Ch | X9) " {y} holds
Intersection F,Ch,y = Intersection F,(Ch | X9),y
let Ch, F 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 set ; :: 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

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 13;
then (Ch | X9) . x in {y} by FUNCT_1:def 13;
then A7: (Ch | X9) . x = y by TARSKI:def 1;
x in dom (Ch | X9) by A6, FUNCT_1:def 13;
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 Th29;
hence Intersection F,Ch,y = Intersection F,(Ch | X9),y by A2, XBOOLE_0:def 10; :: thesis: verum