:: deftheorem defines [:] FUNCOP_1:def 4 :
for F, f being Function
for x being object holds F [:] (f,x) = F * <:f,((dom f) --> x):>;