let C be Category; for I being Indexing of the Source of C, the Target of C holds
( I is Indexing 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) . m2) * ((I `2) . m1) ) ) )
reconsider D = CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) as Category by CAT_5:1;
let I be Indexing of the Source of C, the Target of C; ( I is Indexing 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) . m2) * ((I `2) . m1) ) ) )
A1:
D = CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #)
;
assume that
A4:
for a being Object of C holds (I `2) . (id a) = id ((I `1) . a)
and
A5:
for m1, m2 being Morphism of C st dom m2 = cod m1 holds
(I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1)
; I is Indexing of C
thus
ex D being Category st D = CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #)
by A1; INDEX_1:def 10 ( ( for a being Element of the carrier of C holds (I `2) . ((IdMap C) . a) = id ((I `1) . a) ) & ( for m1, m2 being Element of the carrier' of C st the Source of C . m2 = the Target of C . m1 holds
(I `2) . ( the Comp of C . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1) ) )
let m1, m2 be Morphism of C; ( the Source of C . m2 = the Target of C . m1 implies (I `2) . ( the Comp of C . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1) )
assume
the Source of C . m2 = the Target of C . m1
; (I `2) . ( the Comp of C . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1)
then A6:
dom m2 = cod m1
;
then A7:
(I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1)
by A5;
thus (I `2) . ( the Comp of C . [m2,m1]) =
(I `2) . ( the Comp of C . (m2,m1))
.=
((I `2) . m2) * ((I `2) . m1)
by A6, A7, CAT_1:16
; verum