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)
A1: {} " {y} c= dom {} by RELAT_1:167;
then F | ({} " {y}) = {} ;
then F | ({} " {y}) = ({} " {y}) --> (union (rng F)) by A1;
hence Intersection F,{} ,y = union (rng F) by Th26; :: thesis: verum