:: deftheorem defines renameElementsDistinctlyFunc GLIB_015:def 24 :
for f being Function
for x being object holds renameElementsDistinctlyFunc (f,x) = <:((f . x) --> [f,x]),(id (f . x)):>;