theorem Th27: :: FUNCOP_1:27

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