reconsider T = D as TargetCat of I by A1;
reconsider G = F as Functor of T,E ;
let J1, J2 be Indexing of C; :: thesis: ( ( for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
J1 = (G * (I -functor (C,T))) -indexing_of C ) & ( for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
J2 = (G * (I -functor (C,T))) -indexing_of C ) implies J1 = J2 )
assume A2: ( ( for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
J1 = (G * (I -functor (C,T))) -indexing_of C ) & ( for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
J2 = (G * (I -functor (C,T))) -indexing_of C ) & not J1 = J2 ) ; :: thesis: contradiction
then J1 = (G * (I -functor (C,T))) -indexing_of C ;
hence contradiction by A2; :: thesis: verum