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) #) ;
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) ) )
thus for a being Object of C holds (I `2) . (id a) = id ((I `1) . a) :: thesis: for m1, m2 being Morphism of C st dom m2 = cod m1 holds
(I `2) . (m2 (*) m1) = ((I `2) . m1) * ((I `2) . m2)
proof
let a be Object of C; :: thesis: (I `2) . (id a) = id ((I `1) . a)
id a = (IdMap C) . a by ISOCAT_1:def 12;
hence (I `2) . (id a) = id ((I `1) . a) by A1, Def10, A2; :: thesis: verum
end;
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:15;
(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:16; :: 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) #) by A1; :: according to INDEX_1:def 10 :: thesis: ( ( 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 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) . ((IdMap C) . a) = id ((I `1) . a)
id a = (IdMap C) . a by ISOCAT_1:def 12;
hence (I `2) . ((IdMap 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:16;
A9: [m1,m2] in dom the Comp of C by A7, CAT_1:15;
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