let y, X9 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 object ; :: 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 :: thesis: for x being set st x in dom Ch & Ch . x = y holds
z in F . x
A3: Ch " {y} c= dom (F | X9) by A1, Th19;
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 7;
z in (F | X9) . x by A1, A4, A5, Def2;
hence z in F . x by A6, A3, FUNCT_1:47; :: thesis: verum
end;
( union (rng (F | X9)) c= union (rng F) & z in union (rng (F | X9)) ) by A1, RELAT_1:70, ZFMISC_1:77;
hence z in Intersection (F,Ch,y) by A2, Def2; :: thesis: verum