for X9 being set
for F being Function holds (union (rng F)) /\ X9 = union (rng (Intersect (F,((dom F) --> X9))))