theorem :: FUNCOP_1:31

for g, F being Function
for x being object holds F [;] (x,g) = F .: (((dom g) --> x),g) ;