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

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 13;
then ( dom ((Ch " {y}) --> (union (rng F))) = Ch " {y} & ((Ch " {y}) --> (union (rng F))) . x = union (rng F) ) by FUNCOP_1:13, FUNCOP_1:19;
hence z in F . x by A1, A2, A5, FUNCT_1:70; :: thesis: verum

end;

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

end;

hence Intersection F,Ch,y = union (rng F) by XBOOLE_0:def 10; :: thesis: verum