for f, F being Function
for x, z being object st x in dom (F [;] (z,f)) holds
(F [;] (z,f)) . x = F . (z,(f . x))