let F, Ch be Function; :: thesis: for y being object st F | (Ch " {y}) = (Ch " {y}) --> (union (rng F)) holds
Intersection (F,Ch,y) = union (rng F)
let y be object ; :: thesis: ( F | (Ch " {y}) = (Ch " {y}) --> (union (rng F)) implies Intersection (F,Ch,y) = union (rng F) )
set ChF = (Ch " {y}) --> (union (rng F));
assume A1: F | (Ch " {y}) = (Ch " {y}) --> (union (rng F)) ; :: thesis: Intersection (F,Ch,y) = union (rng F)
union (rng F) c= Intersection (F,Ch,y)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union (rng F) or z in Intersection (F,Ch,y) )
assume A2: z in union (rng F) ; :: 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
A3: x in dom Ch and
A4: Ch . x = y ; :: thesis: z in F . x
Ch . x in {y} by A4, TARSKI:def 1;
then A5: x in Ch " {y} by A3, FUNCT_1:def 7;
then ( dom ((Ch " {y}) --> (union (rng F))) = Ch " {y} & ((Ch " {y}) --> (union (rng F))) . x = union (rng F) ) by FUNCOP_1:7;
hence z in F . x by A1, A2, A5, FUNCT_1:47; :: thesis: verum

end;

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

end;

hence Intersection (F,Ch,y) = union (rng F) ; :: thesis: verum