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) )
reconsider E = {} as set ;
A1: (Ch | E) " {y} c= Ch " {y} by RELAT_1:59, RELAT_1:144;
A2: ( Ch | E = {} & Intersection (F,{},y) = union (rng F) ) by Th28;
assume Ch " {y} = {} ; :: thesis: Intersection (F,Ch,y) = union (rng F)
then (Ch | E) " {y} = Ch " {y} by A1;
hence Intersection (F,Ch,y) = union (rng F) by A2, Th35; :: thesis: verum