theorem Th32: :: FUNCOP_1:32

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))