:: deftheorem Def4 defines commaComp COMMACAT:def 4 :
for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E
for b₆ being PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)) holds
( b₆ = commaComp (F,G) iff ( dom b₆ = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom b₆ holds
b₆ . [k,k9] = k * k9 ) ) );