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 = {} & Intersection (F,{},y) = union (rng F) ) by Th26;
assume Ch " {y} = {} ; :: thesis: Intersection (F,Ch,y) = union (rng F)
then (Ch | E) " {y} = Ch " {y} ;
hence Intersection (F,Ch,y) = union (rng F) by A1, Th33; :: thesis: verum