let C be Category; :: thesis: for D being Categorial Category
for F being Functor of C,D holds D is TargetCat of F -indexing_of C
let D be Categorial Category; :: thesis: for F being Functor of C,D holds D is TargetCat of F -indexing_of C
let F be Functor of C,D; :: thesis: D is TargetCat of F -indexing_of C
set I = F -indexing_of C;
A1: ( (F -indexing_of C) `1 = Obj F & (F -indexing_of C) `2 = pr2 F ) by MCART_1:7;
A2: ( dom F = the carrier' of C & dom (Obj F) = the carrier of C ) by FUNCT_2:def 1;
thus for a being Object of C holds ((F -indexing_of C) `1 ) . a is Object of D by A1, FUNCT_2:7; :: according to INDEX_1:def 9 :: thesis: for b being Element of the carrier' of C holds [[(((F -indexing_of C) `1 ) . (the Source of C . b)),(((F -indexing_of C) `1 ) . (the Target of C . b))],(((F -indexing_of C) `2 ) . b)] is Morphism of D
let b be Morphism of C; :: thesis: [[(((F -indexing_of C) `1 ) . (the Source of C . b)),(((F -indexing_of C) `1 ) . (the Target of C . b))],(((F -indexing_of C) `2 ) . b)] is Morphism of D
set h = F . b;
A3: ( dom (F . b) = (F . b) `11 & cod (F . b) = (F . b) `12 ) by CAT_5:13;
then consider f being Functor of (F . b) `11 ,(F . b) `12 such that
A4: F . b = [[((F . b) `11 ),((F . b) `12 )],f] by CAT_5:def 6;
A5: dom (F . b) = (Obj F) . (dom b) by CAT_1:105
.= (Obj F) . (the Source of C . b) ;
A6: cod (F . b) = (Obj F) . (cod b) by CAT_1:105
.= (Obj F) . (the Target of C . b) ;
((F -indexing_of C) `2 ) . b = (F . b) `2 by A1, A2, MCART_1:def 13
.= f by A4, MCART_1:7 ;
hence [[(((F -indexing_of C) `1 ) . (the Source of C . b)),(((F -indexing_of C) `1 ) . (the Target of C . b))],(((F -indexing_of C) `2 ) . b)] is Morphism of D by A1, A3, A4, A5, A6; :: thesis: verum