theorem :: FUNCOP_1:35

for f being Function
for A being set
for F being Function
for x being object holds (F [;] (x,f)) * (id A) = F [;] (x,(f | A))