:: deftheorem defines CompMap CAT_6:def 29 :
for C being CategoryStr holds CompMap C = the composition of C;