let C, D1, D2, E be Category; 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; 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; 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; ( 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
; 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, Lm6;
I * F = ((I -functor (E,(rng I))) * F9) -indexing_of C
by A1, Def16;
hence
I * F = I * G
by A2, A3, Def16; verum