:: deftheorem defines .: FUNCOP_1:def 3 :
for F, f, g being Function holds F .: (f,g) = F * <:f,g:>;