let C be Category; :: thesis: for I being Indexing of C
for T being TargetCat of I holds Obj (I -functor (C,T)) = I `1
let I be Indexing of C; :: thesis: for T being TargetCat of I holds Obj (I -functor (C,T)) = I `1
let T be TargetCat of I; :: thesis: Obj (I -functor (C,T)) = I `1

A1: now

let x be set ; :: thesis: ( x in the carrier of C implies (Obj (I -functor (C,T))) . x = (I `1) . x )
assume x in the carrier of C ; :: thesis: (Obj (I -functor (C,T))) . x = (I `1) . x
then reconsider a = x as Object of C ;
A2: ( dom (id a) = a & cod (id a) = a ) by CAT_1:44;
(Obj (I -functor (C,T))) . a = dom (id ((Obj (I -functor (C,T))) . a)) by CAT_1:44
.= dom ((I -functor (C,T)) . (id a)) by CAT_1:104
.= ((I -functor (C,T)) . (id a)) `11 by CAT_5:2
.= [[((I `1) . a),((I `1) . a)],((I `2) . (id a))] `11 by A2, Def11 ;
hence (Obj (I -functor (C,T))) . x = (I `1) . x by MCART_1:89; :: thesis: verum

end;

( dom (Obj (I -functor (C,T))) = the carrier of C & dom (I `1) = the carrier of C ) by FUNCT_2:def 1, PARTFUN1:def 4;
hence Obj (I -functor (C,T)) = I `1 by A1, FUNCT_1:9; :: thesis: verum