let C, D1, D2, E be Category; :: thesis: for I being Indexing of E
for F being Functor of C,D1
for G being Functor of C,D2 st Image F is Subcategory of E & Image G is Subcategory of E & F = G holds
I * F = I * G
let I be Indexing of E; :: thesis: for F being Functor of C,D1
for G being Functor of C,D2 st Image F is Subcategory of E & Image G is Subcategory of E & F = G holds
I * F = I * G
let F be Functor of C,D1; :: thesis: for G being Functor of C,D2 st Image F is Subcategory of E & Image G is Subcategory of E & F = G holds
I * F = I * G
let G be Functor of C,D2; :: thesis: ( Image F is Subcategory of E & Image G is Subcategory of E & F = G implies I * F = I * G )
assume A1: ( Image F is Subcategory of E & Image G is Subcategory of E & F = G ) ; :: thesis: I * F = I * G
reconsider F' = F as Functor of C, Image F by CAT_5:8;
reconsider G' = G as Functor of C, Image G by CAT_5:8;
reconsider F' = F', G' = G' as Functor of C,E by A1, Lm5;
( I * F = ((I -functor E,(rng I)) * F') -indexing_of C & I * G = ((I -functor E,(rng I)) * G') -indexing_of C ) by A1, Def16;
hence I * F = I * G by A1; :: thesis: verum