let C be Category; :: thesis: for D being Categorial Category
for F being Functor of C,D
for T being TargetCat of F -indexing_of C holds F = (F -indexing_of C) -functor (C,T)
let D be Categorial Category; :: thesis: for F being Functor of C,D
for T being TargetCat of F -indexing_of C holds F = (F -indexing_of C) -functor (C,T)
let F be Functor of C,D; :: thesis: for T being TargetCat of F -indexing_of C holds F = (F -indexing_of C) -functor (C,T)
set I = F -indexing_of C;
let T be TargetCat of F -indexing_of C; :: thesis: F = (F -indexing_of C) -functor (C,T)
A1: (F -indexing_of C) `2 = pr2 F by MCART_1:7;
A2: dom F = the carrier' of C by FUNCT_2:def 1;
A3: (F -indexing_of C) `1 = Obj F by MCART_1:7;

A4: now

let x be set ; :: thesis: ( x in the carrier' of C implies F . x = ((F -indexing_of C) -functor (C,T)) . x )
assume x in the carrier' of C ; :: thesis: F . x = ((F -indexing_of C) -functor (C,T)) . x
then reconsider f = x as Morphism of C ;
set h = F . f;
A5: ( dom (F . f) = (Obj F) . (dom f) & cod (F . f) = (Obj F) . (cod f) ) by CAT_1:69;
A6: ( dom (F . f) = (F . f) `11 & cod (F . f) = (F . f) `12 ) by CAT_5:13;
then consider g being Functor of (F . f) `11 ,(F . f) `12 such that
A7: F . f = [[((F . f) `11),((F . f) `12)],g] by CAT_5:def 6;
((F -indexing_of C) `2) . f = (F . f) `2 by A1, A2, MCART_1:def 13
.= g by A7, MCART_1:7 ;
hence F . x = ((F -indexing_of C) -functor (C,T)) . x by A3, A6, A7, A5, Def11; :: thesis: verum

end;

dom ((F -indexing_of C) -functor (C,T)) = the carrier' of C by FUNCT_2:def 1;
hence F = (F -indexing_of C) -functor (C,T) by A2, A4, FUNCT_1:2; :: thesis: verum