let C, D be Category; :: thesis: ( [(the carrier of C --> D),(the carrier' of C --> (id D))] is Indexing of C & [(the carrier of C --> D),(the carrier' of C --> (id D))] is coIndexing of C )
set H = [(the carrier of C --> D),(the carrier' of C --> (id D))];
set I = [(the carrier of C --> D),(the carrier' of C --> (id D))];
A1: ( [(the carrier of C --> D),(the carrier' of C --> (id D))] `1 = the carrier of C --> D & [(the carrier of C --> D),(the carrier' of C --> (id D))] `2 = the carrier' of C --> (id D) ) by MCART_1:7;

A2: now

let a be Object of C; :: thesis: ([(the carrier of C --> D),(the carrier' of C --> (id D))] `2 ) . (id a) = id (([(the carrier of C --> D),(the carrier' of C --> (id D))] `1 ) . a)
thus ([(the carrier of C --> D),(the carrier' of C --> (id D))] `2 ) . (id a) = id D by A1, FUNCOP_1:13
.= id (([(the carrier of C --> D),(the carrier' of C --> (id D))] `1 ) . a) by A1, FUNCOP_1:13 ; :: thesis: verum

end;

[(the carrier of C --> D),(the carrier' of C --> (id D))] is Indexing of the Source of C,the Target of C

proof

thus [(the carrier of C --> D),(the carrier' of C --> (id D))] `2 is ManySortedFunctor of ([(the carrier of C --> D),(the carrier' of C --> (id D))] `1 ) * the Source of C,([(the carrier of C --> D),(the carrier' of C --> (id D))] `1 ) * the Target of C :: according to INDEX_1:def 8 :: thesis: verum

proof

thus for m being Morphism of C holds ([(the carrier of C --> D),(the carrier' of C --> (id D))] `2 ) . m is Functor of (([(the carrier of C --> D),(the carrier' of C --> (id D))] `1 ) * the Source of C) . m,(([(the carrier of C --> D),(the carrier' of C --> (id D))] `1 ) * the Target of C) . m by Lm3; :: according to INDEX_1:def 7 :: thesis: verum

end;

end;

then reconsider H = [(the carrier of C --> D),(the carrier' of C --> (id D))] as Indexing of the Source of C,the Target of C ;

now

let m1, m2 be Morphism of C; :: thesis: ( dom m2 = cod m1 implies (H `2 ) . (m2 * m1) = ((H `2 ) . m2) * ((H `2 ) . m1) )
assume dom m2 = cod m1 ; :: thesis: (H `2 ) . (m2 * m1) = ((H `2 ) . m2) * ((H `2 ) . m1)
( (H `2 ) . (m2 * m1) = id D & (H `2 ) . m2 = id D & (H `2 ) . m1 = id D ) by A1, FUNCOP_1:13;
hence (H `2 ) . (m2 * m1) = ((H `2 ) . m2) * ((H `2 ) . m1) by FUNCT_2:23; :: thesis: verum

end;

hence [(the carrier of C --> D),(the carrier' of C --> (id D))] is Indexing of C by A2, Th6; :: thesis: [(the carrier of C --> D),(the carrier' of C --> (id D))] is coIndexing of C
H is Indexing of the Target of C,the Source of C

proof

thus H `2 is ManySortedFunctor of (H `1 ) * the Target of C,(H `1 ) * the Source of C :: according to INDEX_1:def 8 :: thesis: verum

proof

thus for m being Morphism of C holds (H `2 ) . m is Functor of ((H `1 ) * the Target of C) . m,((H `1 ) * the Source of C) . m by Lm4; :: according to INDEX_1:def 7 :: thesis: verum

end;

end;

then reconsider H = H as Indexing of the Target of C,the Source of C ;

now

let m1, m2 be Morphism of C; :: thesis: ( dom m2 = cod m1 implies (H `2 ) . (m2 * m1) = ((H `2 ) . m1) * ((H `2 ) . m2) )
assume dom m2 = cod m1 ; :: thesis: (H `2 ) . (m2 * m1) = ((H `2 ) . m1) * ((H `2 ) . m2)
( (H `2 ) . (m2 * m1) = id D & (H `2 ) . m2 = id D & (H `2 ) . m1 = id D ) by A1, FUNCOP_1:13;
hence (H `2 ) . (m2 * m1) = ((H `2 ) . m1) * ((H `2 ) . m2) by FUNCT_2:23; :: thesis: verum

end;

hence [(the carrier of C --> D),(the carrier' of C --> (id D))] is coIndexing of C by A2, Th7; :: thesis: verum