theorem Th7: :: INDEX_1:7

for C being Category
for I being Indexing of the Target of C, the Source of C holds
( I is coIndexing of C iff ( ( for a being Object of C holds (I `2) . (id a) = id ((I `1) . a) ) & ( for m1, m2 being Morphism of C st dom m2 = cod m1 holds
(I `2) . (m2 (*) m1) = ((I `2) . m1) * ((I `2) . m2) ) ) )