let C be Category; :: thesis: 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, the Id of C #) as Category by CAT_5:1;
let I be Indexing of the Source of C, the Target of C; :: thesis: ( 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, the Id of C #) ;

hereby :: thesis: ( ( 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) ) implies I is Indexing of C )

assume A2: I is Indexing of C ; :: thesis: ( ( 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) ) )
hence for a being Object of C holds (I `2) . (id a) = id ((I `1) . a) by A1, Def10; :: thesis: for m1, m2 being Morphism of C st dom m2 = cod m1 holds
(I `2) . (m2 * m1) = ((I `2) . m2) * ((I `2) . m1)
let m1, m2 be Morphism of C; :: thesis: ( dom m2 = cod m1 implies (I `2) . (m2 * m1) = ((I `2) . m2) * ((I `2) . m1) )
assume A3: dom m2 = cod m1 ; :: thesis: (I `2) . (m2 * m1) = ((I `2) . m2) * ((I `2) . m1)
then (I `2) . ( the Comp of C . (m2,m1)) = ((I `2) . m2) * ((I `2) . m1) by A1, A2, Def10;
hence (I `2) . (m2 * m1) = ((I `2) . m2) * ((I `2) . m1) by A3, CAT_1:16; :: thesis: verum

end;

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) ; :: thesis: 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, the Id of C #) by A1; :: according to INDEX_1:def 10 :: thesis: ( ( for a being Element of the carrier of C holds (I `2) . ( the Id of 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) ) )

hereby :: thesis: 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 a be Object of C; :: thesis: (I `2) . ( the Id of C . a) = id ((I `1) . a)
thus (I `2) . ( the Id of C . a) = (I `2) . (id a)
.= id ((I `1) . a) by A4 ; :: thesis: verum

end;

let m1, m2 be Morphism of C; :: thesis: ( 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 ; :: thesis: (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 ; :: thesis: verum