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: dom F = the carrier' of C by FUNCT_2:def 1;
dom (Obj F) = the carrier of C by FUNCT_2:def 1;
then A2: Obj F is ManySortedSet of the carrier of C by PARTFUN1:def 2;
A3: [(Obj F),(pr2 F)] `2 = pr2 F ;
A4: dom (pr2 F) = dom F by MCART_1:def 13;
then pr2 F is ManySortedSet of the carrier' of C by A1, PARTFUN1:def 2, RELAT_1:def 18;
then reconsider I = [(Obj F),(pr2 F)] as ManySortedSet of the carrier of C, the carrier' of C by A2, Def4;
pr2 F is Function-yielding

proof

let x be object ; :: 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 A1, MCART_1:def 13;
reconsider m = F . x as Morphism of D ;
(pr2 F) . x = m `2 by A1, 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 A4, A1, PARTFUN1:def 2, RELAT_1:def 18;
I `1 is Category-yielding ;
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 ;
A5: 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
A6: F . m = [[(x `11),(x `12)],f] by A5, CAT_5:def 6;
A7: ((Obj F) * the Source of C) . m = (Obj F) . (dom m) by FUNCT_2:15
.= dom (F . m) by CAT_1:69 ;
A8: ((Obj F) * the Target of C) . m = (Obj F) . (cod m) by FUNCT_2:15
.= cod (F . m) by CAT_1:69 ;
FF . m = x `2 by A1, MCART_1:def 13
.= f by A6 ;
hence FF . m is Functor of ((I `1) * the Source of C) . m,((I `1) * the Target of C) . m by A5, A7, A8, CAT_5:13; :: thesis: verum

end;

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

A10: now :: thesis: for m1, m2 being Morphism of C st dom m2 = cod m1 holds
(I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1)

let m1, m2 be Morphism of C; :: thesis: ( dom m2 = cod m1 implies (I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1) )
assume A11: dom m2 = cod m1 ; :: thesis: (I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1)
set h1 = F . m1;
set h2 = F . m2;
A12: dom (F . m2) = F . (dom m2) by CAT_1:72
.= cod (F . m1) by A11, CAT_1:72 ;
A13: 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
A14: F . m2 = [[((F . m2) `11),((F . m2) `12)],f2] by A13, CAT_5:def 6;
A15: 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
A16: F . m1 = [[((F . m1) `11),((F . m1) `12)],f1] by A15, CAT_5:def 6;
thus (I `2) . (m2 (*) m1) = (F . (m2 (*) m1)) `2 by A9, MCART_1:def 13
.= ((F . m2) (*) (F . m1)) `2 by A11, CAT_1:64
.= [[((F . m1) `11),((F . m2) `12)],(f2 * f1)] `2 by A13, A15, A14, A16, A12, CAT_5:def 6
.= f2 * f1
.= ((F . m2) `2) * f1 by A14
.= ((F . m2) `2) * ((F . m1) `2) by A16
.= ((I `2) . m2) * ((F . m1) `2) by A9, MCART_1:def 13
.= ((I `2) . m2) * ((I `2) . m1) by A9, MCART_1:def 13 ; :: thesis: verum

end;

now :: thesis: for a being Object of C holds (I `2) . (id a) = id ((I `1) . a)

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 A9, MCART_1:def 13
.= (id i) `2 by CAT_1:68
.= [[((I `1) . a),((I `1) . a)],(id ((I `1) . a))] `2 by CAT_5:def 6
.= id ((I `1) . a) ; :: thesis: verum

end;

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