let y be set ; :: thesis: for Ch, F being Function st Ch " {y} = {} holds
Intersection F,Ch,y = union (rng F)
let Ch, F be Function; :: thesis: ( Ch " {y} = {} implies Intersection F,Ch,y = union (rng F) )
assume A1: Ch " {y} = {} ; :: thesis: Intersection F,Ch,y = union (rng F)
reconsider E = {} as set ;
(Ch | E) " {y} c= Ch " {y} by RELAT_1:88, RELAT_1:179;
then ( (Ch | E) " {y} = Ch " {y} & Ch | E = {} & Intersection F,{} ,y = union (rng F) ) by A1, Th28;
hence Intersection F,Ch,y = union (rng F) by Th35; :: thesis: verum