:: deftheorem Def3 defines * COMMACAT:def 3 :
for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E
for k1, k2 being Element of commaMorphs (F,G) st ex c1 being Object of C ex d1 being Object of D ex f1 being Morphism of E st f1 in Hom ((F . c1),(G . d1)) & k1 `12 = k2 `11 holds
k2 * k1 = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]];