reconsider A = Image F as Subcategory of E by A1;
reconsider G = F as Functor of C,A by CAT_5:8;
let J1, J2 be Indexing of C; :: thesis: ( ( for F9 being Functor of C,E st F9 = F holds
J1 = ((I -functor (E,(rng I))) * F9) -indexing_of C ) & ( for F9 being Functor of C,E st F9 = F holds
J2 = ((I -functor (E,(rng I))) * F9) -indexing_of C ) implies J1 = J2 )
assume that
A2: for F9 being Functor of C,E st F9 = F holds
J1 = ((I -functor (E,(rng I))) * F9) -indexing_of C and
A3: for F9 being Functor of C,E st F9 = F holds
J2 = ((I -functor (E,(rng I))) * F9) -indexing_of C ; :: thesis: J1 = J2
reconsider G = G as Functor of C,E by Lm6;
thus J1 = ((I -functor (E,(rng I))) * G) -indexing_of C by A2
.= J2 by A3 ; :: thesis: verum