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

now

let x be set ; :: thesis: ( x in dom (Ch | X9) & (Ch | X9) . x = y implies z in F . x )
assume that
A2: x in dom (Ch | X9) and
A3: (Ch | X9) . x = y ; :: thesis: z in F . x
x in (dom Ch) /\ X9 by A2, RELAT_1:90;
then A4: x in dom Ch by XBOOLE_0:def 4;
Ch . x = y by A2, A3, FUNCT_1:70;
hence z in F . x by A1, A4, Def2; :: thesis: verum

end;

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