let C be Category; :: thesis: for D being Categorial Category
for F being Functor of C,D holds [(Obj F),(pr2 F)] is Indexing of C
let D be Categorial Category; :: thesis: for F being Functor of C,D holds [(Obj F),(pr2 F)] is Indexing of C
let F be Functor of C,D; :: thesis: [(Obj F),(pr2 F)] is Indexing of C
set I = [(Obj F),(pr2 F)];
A1: [(Obj F),(pr2 F)] `1 = Obj F by MCART_1:7;
A2: dom F = the carrier' of C by FUNCT_2:def 1;
dom (Obj F) = the carrier of C by FUNCT_2:def 1;
then A3: Obj F is ManySortedSet of the carrier of C by PARTFUN1:def 4;
A4: [(Obj F),(pr2 F)] `2 = pr2 F by MCART_1:7;
A5: dom (pr2 F) = dom F by MCART_1:def 13;
then pr2 F is ManySortedSet of the carrier' of C by A2, PARTFUN1:def 4, RELAT_1:def 18;
then reconsider I = [(Obj F),(pr2 F)] as ManySortedSet of the carrier of C,the carrier' of C by A3, Def4;
pr2 F is Function-yielding

proof

let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 (pr2 F) or (pr2 F) . x is set )
assume x in dom (pr2 F) ; :: thesis: (pr2 F) . x is set
then reconsider x = x as Morphism of C by A2, MCART_1:def 13;
reconsider m = F . x as Morphism of D ;
(pr2 F) . x = m `2 by A2, MCART_1:def 13;
hence (pr2 F) . x is set ; :: thesis: verum

end;

then reconsider FF = pr2 F as ManySortedFunction of the carrier' of C by A5, A2, PARTFUN1:def 4, RELAT_1:def 18;
I `1 is Category-yielding by MCART_1:7;
then reconsider I = I as Category-yielding_on_first ManySortedSet of the carrier of C,the carrier' of C by Def5;
FF is ManySortedFunctor of (I `1 ) * the Source of C,(I `1 ) * the Target of C

proof

let m be Morphism of C; :: according to INDEX_1:def 7 :: thesis: FF . m is Functor of ((I `1 ) * the Source of C) . m,((I `1 ) * the Target of C) . m
reconsider x = F . m as Morphism of D ;
A6: x `11 = dom (F . m) by CAT_5:13;
x `12 = cod (F . m) by CAT_5:13;
then consider f being Functor of x `11 ,x `12 such that
A7: F . m = [[(x `11 ),(x `12 )],f] by A6, CAT_5:def 6;
A8: ((Obj F) * the Source of C) . m = (Obj F) . (dom m) by FUNCT_2:21
.= dom (F . m) by CAT_1:105 ;
A9: ((Obj F) * the Target of C) . m = (Obj F) . (cod m) by FUNCT_2:21
.= cod (F . m) by CAT_1:105 ;
FF . m = x `2 by A2, MCART_1:def 13
.= f by A7, MCART_1:7 ;
hence FF . m is Functor of ((I `1 ) * the Source of C) . m,((I `1 ) * the Target of C) . m by A1, A6, A8, A9, CAT_5:13; :: thesis: verum

end;

then reconsider I = I as Indexing of the Source of C,the Target of C by A4, Def8;
A10: dom F = the carrier' of C by FUNCT_2:def 1;

A11: now

let m1, m2 be Morphism of C; :: thesis: ( dom m2 = cod m1 implies (I `2 ) . (m2 * m1) = ((I `2 ) . m2) * ((I `2 ) . m1) )
assume A12: dom m2 = cod m1 ; :: thesis: (I `2 ) . (m2 * m1) = ((I `2 ) . m2) * ((I `2 ) . m1)
set h1 = F . m1;
set h2 = F . m2;
A13: dom (F . m2) = F . (dom m2) by CAT_1:109
.= cod (F . m1) by A12, CAT_1:109 ;
A14: dom (F . m2) = (F . m2) `11 by CAT_5:13;
cod (F . m2) = (F . m2) `12 by CAT_5:13;
then consider f2 being Functor of (F . m2) `11 ,(F . m2) `12 such that
A15: F . m2 = [[((F . m2) `11 ),((F . m2) `12 )],f2] by A14, CAT_5:def 6;
A16: cod (F . m1) = (F . m1) `12 by CAT_5:13;
dom (F . m1) = (F . m1) `11 by CAT_5:13;
then consider f1 being Functor of (F . m1) `11 ,(F . m1) `12 such that
A17: F . m1 = [[((F . m1) `11 ),((F . m1) `12 )],f1] by A16, CAT_5:def 6;
thus (I `2 ) . (m2 * m1) = (F . (m2 * m1)) `2 by A4, A10, MCART_1:def 13
.= ((F . m2) * (F . m1)) `2 by A12, CAT_1:99
.= [[((F . m1) `11 ),((F . m2) `12 )],(f2 * f1)] `2 by A14, A16, A15, A17, A13, CAT_5:def 6
.= f2 * f1 by MCART_1:7
.= ((F . m2) `2 ) * f1 by A15, MCART_1:7
.= ((F . m2) `2 ) * ((F . m1) `2 ) by A17, MCART_1:7
.= ((I `2 ) . m2) * ((F . m1) `2 ) by A4, A10, MCART_1:def 13
.= ((I `2 ) . m2) * ((I `2 ) . m1) by A4, A10, MCART_1:def 13 ; :: thesis: verum

end;

now

let a be Object of C; :: thesis: (I `2 ) . (id a) = id ((I `1 ) . a)
reconsider i = (Obj F) . a as Object of D ;
thus (I `2 ) . (id a) = (F . (id a)) `2 by A4, A10, MCART_1:def 13
.= (id i) `2 by CAT_1:104
.= [[((I `1 ) . a),((I `1 ) . a)],(id ((I `1 ) . a))] `2 by A1, CAT_5:def 6
.= id ((I `1 ) . a) by MCART_1:7 ; :: thesis: verum

end;

hence [(Obj F),(pr2 F)] is Indexing of C by A11, Th6; :: thesis: verum