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