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;
let J1, J2 be Indexing of C; :: thesis: ( ( for F' being Functor of C,E st F' = F holds
J1 = ((I -functor E,(rng I)) * F') -indexing_of C ) & ( for F' being Functor of C,E st F' = F holds
J2 = ((I -functor E,(rng I)) * F') -indexing_of C ) implies J1 = J2 )
assume that
A2: for F' being Functor of C,E st F' = F holds
J1 = ((I -functor E,(rng I)) * F') -indexing_of C and
A3: for F' being Functor of C,E st F' = F holds
J2 = ((I -functor E,(rng I)) * F') -indexing_of C ; :: thesis: J1 = J2
thus J1 = ((I -functor E,(rng I)) * G) -indexing_of C by A2
.= J2 by A3 ; :: thesis: verum