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: now :: thesis: for x being object st x in the carrier' of C holds
(I -functor (C,T1)) . x = (I -functor (C,T2)) . x

let x be object ; :: 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;

thus I -functor (C,T1) = I -functor (C,T2) by A1; :: thesis: Obj (I -functor (C,T1)) = Obj (I -functor (C,T2))

A2: now :: thesis: for x being object st x in the carrier of C holds
(Obj (I -functor (C,T1))) . x = (Obj (I -functor (C,T2))) . x

let x be object ; :: 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 Lm3
.= (Obj (I -functor (C,T2))) . x by Lm3 ; :: thesis: verum

end;

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