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))] `2 = the carrier' of C --> (id D) by MCART_1:7;
A2: [(the carrier of C --> D),(the carrier' of C --> (id D))] `1 = the carrier of C --> D by MCART_1:7;

A3: 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 A2, FUNCOP_1:13 ; :: thesis: verum

end;

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;
then [(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 by Def7;
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 by Def8;

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)
A4: (H `2 ) . m1 = id D by A1, FUNCOP_1:13;
( (H `2 ) . (m2 * m1) = id D & (H `2 ) . m2 = id D ) by A1, FUNCOP_1:13;
hence (H `2 ) . (m2 * m1) = ((H `2 ) . m2) * ((H `2 ) . m1) by A4, FUNCT_2:23; :: thesis: verum

end;

hence [(the carrier of C --> D),(the carrier' of C --> (id D))] is Indexing of C by A3, Th6; :: thesis: [(the carrier of C --> D),(the carrier' of C --> (id D))] is coIndexing of C
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;
then H `2 is ManySortedFunctor of (H `1 ) * the Target of C,(H `1 ) * the Source of C by Def7;
then reconsider H = H as Indexing of the Target of C,the Source of C by Def8;

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)
A5: (H `2 ) . m1 = id D by A1, FUNCOP_1:13;
( (H `2 ) . (m2 * m1) = id D & (H `2 ) . m2 = id D ) by A1, FUNCOP_1:13;
hence (H `2 ) . (m2 * m1) = ((H `2 ) . m1) * ((H `2 ) . m2) by A5, FUNCT_2:23; :: thesis: verum

end;

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