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