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