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