:: deftheorem defines . INDEX_1:def 14 :
for C being Category
for I being coIndexing of C
for m being Morphism of C holds I . m = (I `2) . m;