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 :: thesis: for x being object st x in the carrier of C holds
(Obj (I -functor (C,T))) . x = (I `1) . x
let x be object ; :: 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 ) ;
(Obj (I -functor (C,T))) . a = dom (id ((Obj (I -functor (C,T))) . a))
.= dom ((I -functor (C,T)) . (id a)) by CAT_1:68
.= ((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:85; :: 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 2;
hence Obj (I -functor (C,T)) = I `1 by A1; :: thesis: verum