let F be Function; :: thesis: for y being object holds Intersection (F,{},y) = union (rng F)
let y be object ; :: thesis: Intersection (F,{},y) = union (rng F)
F | ({} " {y}) = ({} " {y}) --> (union (rng F)) ;
hence Intersection (F,{},y) = union (rng F) by Th23; :: thesis: verum