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