theorem Th80: :: GLIB_015:80

for f being Function
for x being object holds rng (renameElementsDistinctlyFunc (f,x)) = [:{[f,x]},(f . x):]