reconsider T = D as TargetCat of I by A1;
reconsider G = F as Functor of T,E ;
take (G * (I -functor (C,T))) -indexing_of C ; :: thesis: for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
(G * (I -functor (C,T))) -indexing_of C = (G * (I -functor (C,T))) -indexing_of C
thus for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
(G * (I -functor (C,T))) -indexing_of C = (G * (I -functor (C,T))) -indexing_of C ; :: thesis: verum