let C be Category; :: thesis: 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) ) ) )
let I be Indexing of the Target of C,the Source of C; :: thesis: ( 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) ) ) )
A1: C opp = CatStr(# the carrier of C,the carrier' of C,the Target of C,the Source of C,(~ the Comp of C),the Id of C #) by OPPCAT_1:def 1;

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 ) . m1) * ((I `2 ) . m2) ) implies I is coIndexing of C )

assume A2: I is coIndexing 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 ) . m1) * ((I `2 ) . m2) ) )
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 ) . m1) * ((I `2 ) . m2)
let m1, m2 be Morphism of C; :: thesis: ( dom m2 = cod m1 implies (I `2 ) . (m2 * m1) = ((I `2 ) . m1) * ((I `2 ) . m2) )
assume A3: dom m2 = cod m1 ; :: thesis: (I `2 ) . (m2 * m1) = ((I `2 ) . m1) * ((I `2 ) . m2)
then A4: [m2,m1] in dom the Comp of C by CAT_1:40;
(I `2 ) . ((~ the Comp of C) . m1,m2) = ((I `2 ) . m1) * ((I `2 ) . m2) by A1, A2, A3, Def10;
then (I `2 ) . (the Comp of C . m2,m1) = ((I `2 ) . m1) * ((I `2 ) . m2) by A4, FUNCT_4:def 2;
hence (I `2 ) . (m2 * m1) = ((I `2 ) . m1) * ((I `2 ) . m2) by A3, CAT_1:41; :: thesis: verum

end;

assume that
A5: for a being Object of C holds (I `2 ) . (id a) = id ((I `1 ) . a) and
A6: for m1, m2 being Morphism of C st dom m2 = cod m1 holds
(I `2 ) . (m2 * m1) = ((I `2 ) . m1) * ((I `2 ) . m2) ; :: thesis: I is coIndexing of C
thus ex D being Category st D = CatStr(# the carrier of C,the carrier' of C,the Target of C,the Source 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 Target of C . m2 = the Source 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 Target of C . m2 = the Source 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 A5 ; :: thesis: verum

end;

let m1, m2 be Morphism of C; :: thesis: ( the Target of C . m2 = the Source of C . m1 implies (I `2 ) . ((~ the Comp of C) . [m2,m1]) = ((I `2 ) . m2) * ((I `2 ) . m1) )
assume the Target of C . m2 = the Source of C . m1 ; :: thesis: (I `2 ) . ((~ the Comp of C) . [m2,m1]) = ((I `2 ) . m2) * ((I `2 ) . m1)
then A7: dom m1 = cod m2 ;
then (I `2 ) . (m1 * m2) = ((I `2 ) . m2) * ((I `2 ) . m1) by A6;
then A8: (I `2 ) . (the Comp of C . m1,m2) = ((I `2 ) . m2) * ((I `2 ) . m1) by A7, CAT_1:41;
A9: [m1,m2] in dom the Comp of C by A7, CAT_1:40;
thus (I `2 ) . ((~ the Comp of C) . [m2,m1]) = (I `2 ) . ((~ the Comp of C) . m2,m1)
.= ((I `2 ) . m2) * ((I `2 ) . m1) by A8, A9, FUNCT_4:def 2 ; :: thesis: verum