theorem Th79: :: GLIB_015:79

for f being Function
for x, z being object st x in dom f & z in rng (renameElementsDistinctlyFunc (f,x)) holds
ex y being object st
( y in f . x & z = [f,x,y] )