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 Lm6;
take ((I -functor (E,(rng I))) * G) -indexing_of C ; :: thesis: for F9 being Functor of C,E st F9 = F holds
((I -functor (E,(rng I))) * G) -indexing_of C = ((I -functor (E,(rng I))) * F9) -indexing_of C
thus for F9 being Functor of C,E st F9 = F holds
((I -functor (E,(rng I))) * G) -indexing_of C = ((I -functor (E,(rng I))) * F9) -indexing_of C ; :: thesis: verum