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;
thus for a being Object of C holds ((F -indexing_of C) `1) . a is Object of D by FUNCT_2:5; :: 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;
A1: dom (F . b) = (F . b) `11 by CAT_5:13;
cod (F . b) = (F . b) `12 by CAT_5:13;
then consider f being Functor of (F . b) `11 ,(F . b) `12 such that
A2: F . b = [[((F . b) `11),((F . b) `12)],f] by A1, CAT_5:def 6;
A3: cod (F . b) = (Obj F) . (cod b) by CAT_1:69
.= (Obj F) . ( the Target of C . b) ;
A4: dom (F . b) = (Obj F) . (dom b) by CAT_1:69
.= (Obj F) . ( the Source of C . b) ;
( (F -indexing_of C) `2 = pr2 F & dom F = the carrier' of C ) by FUNCT_2:def 1;
then ((F -indexing_of C) `2) . b = (F . b) `2 by MCART_1:def 13
.= f by A2 ;
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, A2, A4, A3, CAT_5:13; :: thesis: verum