reconsider A = Image F as Subcategory of E by A1;
reconsider G = F as Functor of C,A by CAT_5:8;
reconsider G = G as Functor of C,E by Lm5;
take ((I -functor E,(rng I)) * G) -indexing_of C ; :: thesis: for F' being Functor of C,E st F' = F holds
((I -functor E,(rng I)) * G) -indexing_of C = ((I -functor E,(rng I)) * F') -indexing_of C
thus for F' being Functor of C,E st F' = F holds
((I -functor E,(rng I)) * G) -indexing_of C = ((I -functor E,(rng I)) * F') -indexing_of C ; :: thesis: verum