let y be set ; :: thesis: for F being Function holds Intersection F,{} ,y = union (rng F)
let F be Function; :: thesis: Intersection F,{} ,y = union (rng F)
( {} " {y} c= dom {} & dom {} = {} ) by RELAT_1:167;
then {} " {y} = {} ;
then ( F | ({} " {y}) = {} & dom (({} " {y}) --> (union (rng F))) = {} ) ;
then F | ({} " {y}) = ({} " {y}) --> (union (rng F)) ;
hence Intersection F,{} ,y = union (rng F) by Th26; :: thesis: verum