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 that
A1: Image F is Subcategory of E and
A2: Image G is Subcategory of E and
A3: F = G ; :: thesis: I * F = I * G
reconsider G' = G as Functor of C, Image G by CAT_5:8;
reconsider F' = F as Functor of C, Image F by CAT_5:8;
reconsider F' = F', G' = G' as Functor of C,E by A1, A2, Lm5;
I * F = ((I -functor E,(rng I)) * F') -indexing_of C by A1, Def16;
hence I * F = I * G by A2, A3, Def16; :: thesis: verum