theorem :: FUNCOP_1:26

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