let C be Category; :: thesis: for I being Indexing of C
for T1, T2 being TargetCat of I holds
( I -functor C,T1 = I -functor C,T2 & Obj (I -functor C,T1) = Obj (I -functor C,T2) )
let I be Indexing of C; :: thesis: for T1, T2 being TargetCat of I holds
( I -functor C,T1 = I -functor C,T2 & Obj (I -functor C,T1) = Obj (I -functor C,T2) )
let T1, T2 be TargetCat of I; :: thesis: ( I -functor C,T1 = I -functor C,T2 & Obj (I -functor C,T1) = Obj (I -functor C,T2) )
A1: ( dom (I -functor C,T1) = the carrier' of C & dom (I -functor C,T2) = the carrier' of C ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in the carrier' of C implies (I -functor C,T1) . x = (I -functor C,T2) . x )
assume x in the carrier' of C ; :: thesis: (I -functor C,T1) . x = (I -functor C,T2) . x
then reconsider f = x as Morphism of C ;
thus (I -functor C,T1) . x = [[((I `1 ) . (dom f)),((I `1 ) . (cod f))],((I `2 ) . f)] by Def11
.= (I -functor C,T2) . x by Def11 ; :: thesis: verum

end;

hence I -functor C,T1 = I -functor C,T2 by A1, FUNCT_1:9; :: thesis: Obj (I -functor C,T1) = Obj (I -functor C,T2)
A2: ( dom (Obj (I -functor C,T1)) = the carrier of C & dom (Obj (I -functor C,T2)) = the carrier of C ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in the carrier of C implies (Obj (I -functor C,T1)) . x = (Obj (I -functor C,T2)) . x )
assume x in the carrier of C ; :: thesis: (Obj (I -functor C,T1)) . x = (Obj (I -functor C,T2)) . x
then reconsider a = x as Object of C ;
thus (Obj (I -functor C,T1)) . x = (I `1 ) . a by Lm2
.= (Obj (I -functor C,T2)) . x by Lm2 ; :: thesis: verum

end;

hence Obj (I -functor C,T1) = Obj (I -functor C,T2) by A2, FUNCT_1:9; :: thesis: verum