let X9 be set ; :: thesis: for F, Ch being Function
for y being object holds Intersection (F,Ch,y) c= Intersection (F,(Ch | X9),y)
let F, Ch be Function; :: thesis: for y being object holds Intersection (F,Ch,y) c= Intersection (F,(Ch | X9),y)
let y be object ; :: thesis: Intersection (F,Ch,y) c= Intersection (F,(Ch | X9),y)
let z be object ; :: 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 :: thesis: for x being set st x in dom (Ch | X9) & (Ch | X9) . x = y holds
z in F . x

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:61;
then A4: x in dom Ch by XBOOLE_0:def 4;
Ch . x = y by A2, A3, FUNCT_1:47;
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