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: dom F = the carrier' of C by FUNCT_2:def 1;
A2: now :: thesis: for x being object st x in the carrier' of C holds
F . x = ((F -indexing_of C) -functor (C,T)) . x
let x be object ; :: 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;
A3: ( dom (F . f) = (Obj F) . (dom f) & cod (F . f) = (Obj F) . (cod f) ) by CAT_1:69;
A4: ( 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
A5: 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, MCART_1:def 13
.= g by A5 ;
hence F . x = ((F -indexing_of C) -functor (C,T)) . x by A4, A5, A3, Def11; :: thesis: verum
end;
thus F = (F -indexing_of C) -functor (C,T) by A2; :: thesis: verum