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:7
.= id (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . a) by A2, FUNCOP_1:7 ; :: 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:7;
( (H `2) . (m2 * m1) = id D & (H `2) . m2 = id D ) by A1, FUNCOP_1:7;
hence (H `2) . (m2 * m1) = ((H `2) . m2) * ((H `2) . m1) by A4, FUNCT_2:17; :: 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:7;
( (H `2) . (m2 * m1) = id D & (H `2) . m2 = id D ) by A1, FUNCOP_1:7;
hence (H `2) . (m2 * m1) = ((H `2) . m1) * ((H `2) . m2) by A5, FUNCT_2:17; :: thesis: verum

end;

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