theorem :: GLIB_015:81

for f being Function
for x1, x2 being object holds rng (renameElementsDistinctlyFunc (f,x1)) misses f . x2