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: ( 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;

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;

hence Obj (I -functor C,T) = I `1 by A1, FUNCT_1:9; :: thesis: verum