:: deftheorem Def4 defines the_comps_of ALTCAT_2:def 4 :
for C being Category
for b₂ being BinComp of (the_hom_sets_of C) holds
( b₂ = the_comps_of C iff for i, j, k being Object of C holds b₂ . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] );