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

proof

let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in dom (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 A3;
reconsider m = F . x as Morphism of D ;
(pr2 F) . x = m `2 by A3, MCART_1:def 13;
hence (pr2 F) . x is set ; :: thesis: verum

end;

then reconsider FF = pr2 F as ManySortedFunction of by A3, PARTFUN1:def 4, RELAT_1:def 18;
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 ;
A4: ( x `11 = dom (F . m) & x `12 = cod (F . m) ) by CAT_5:13;
then consider f being Functor of x `11 ,x `12 such that
A5: F . m = [[(x `11 ),(x `12 )],f] by CAT_5:def 6;
A6: FF . m = x `2 by A3, MCART_1:def 13
.= f by A5, MCART_1:7 ;
A7: ((Obj F) * the Source of C) . m = (Obj F) . (dom m) by FUNCT_2:21
.= dom (F . m) by CAT_1:105 ;
((Obj F) * the Target of C) . m = (Obj F) . (cod m) by FUNCT_2:21
.= cod (F . m) by CAT_1:105 ;
hence FF . m is Functor of ((I `1 ) * the Source of C) . m,((I `1 ) * the Target of C) . m by A1, A4, A6, A7; :: thesis: verum

end;

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

A9: 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 A1, A8, 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;

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 A10: dom m2 = cod m1 ; :: thesis: (I `2 ) . (m2 * m1) = ((I `2 ) . m2) * ((I `2 ) . m1)
set h1 = F . m1;
set h2 = F . m2;
A11: ( dom (F . m2) = (F . m2) `11 & cod (F . m2) = (F . m2) `12 & dom (F . m1) = (F . m1) `11 & cod (F . m1) = (F . m1) `12 ) by CAT_5:13;
then consider f2 being Functor of (F . m2) `11 ,(F . m2) `12 such that
A12: F . m2 = [[((F . m2) `11 ),((F . m2) `12 )],f2] by CAT_5:def 6;
consider f1 being Functor of (F . m1) `11 ,(F . m1) `12 such that
A13: F . m1 = [[((F . m1) `11 ),((F . m1) `12 )],f1] by A11, CAT_5:def 6;
A14: dom (F . m2) = F . (dom m2) by CAT_1:109
.= cod (F . m1) by A10, CAT_1:109 ;
thus (I `2 ) . (m2 * m1) = (F . (m2 * m1)) `2 by A1, A8, MCART_1:def 13
.= ((F . m2) * (F . m1)) `2 by A10, CAT_1:99
.= [[((F . m1) `11 ),((F . m2) `12 )],(f2 * f1)] `2 by A11, A12, A13, A14, CAT_5:def 6
.= f2 * f1 by MCART_1:7
.= ((F . m2) `2 ) * f1 by A12, MCART_1:7
.= ((F . m2) `2 ) * ((F . m1) `2 ) by A13, MCART_1:7
.= ((I `2 ) . m2) * ((F . m1) `2 ) by A1, A8, MCART_1:def 13
.= ((I `2 ) . m2) * ((I `2 ) . m1) by A1, A8, MCART_1:def 13 ; :: thesis: verum

end;

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