:: deftheorem Def1 defines (*) CAT_1:def 1 :
for C being CatStr
for f, g being Morphism of C st [g,f] in dom the Comp of C holds
g (*) f = the Comp of C . (g,f);