let C, D be Category; ( [( 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:
for a being Object of C holds ([( 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)
;
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 Lm4;
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;
for m1, m2 being Morphism of C st dom m2 = cod m1 holds
(H `2) . (m2 (*) m1) = ((H `2) . m2) * ((H `2) . m1)
by FUNCT_2:17;
hence
[( the carrier of C --> D),( the carrier' of C --> (id D))] is Indexing of C
by A1, Th6; [( 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 Lm5;
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;
for m1, m2 being Morphism of C st dom m2 = cod m1 holds
(H `2) . (m2 (*) m1) = ((H `2) . m1) * ((H `2) . m2)
by FUNCT_2:17;
hence
[( the carrier of C --> D),( the carrier' of C --> (id D))] is coIndexing of C
by A1, Th7; verum