theorem Th78: :: GLIB_015:78

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