let F, Ch be Function; for y being object st F | (Ch " {y}) = (Ch " {y}) --> (union (rng F)) holds
Intersection (F,Ch,y) = union (rng F)
let y be object ; ( F | (Ch " {y}) = (Ch " {y}) --> (union (rng F)) implies Intersection (F,Ch,y) = union (rng F) )
set ChF = (Ch " {y}) --> (union (rng F));
assume A1:
F | (Ch " {y}) = (Ch " {y}) --> (union (rng F))
; Intersection (F,Ch,y) = union (rng F)
union (rng F) c= Intersection (F,Ch,y)
hence
Intersection (F,Ch,y) = union (rng F)
; verum