let C be Category; 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; for T being TargetCat of I holds Obj (I -functor (C,T)) = I `1
let T be TargetCat of I; Obj (I -functor (C,T)) = I `1
A1:
now for x being object st x in the carrier of C holds
(Obj (I -functor (C,T))) . x = (I `1) . xlet x be
object ;
( x in the carrier of C implies (Obj (I -functor (C,T))) . x = (I `1) . x )assume
x in the
carrier of
C
;
(Obj (I -functor (C,T))) . x = (I `1) . xthen 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;
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; verum