let C be Category; for I being Indexing of C
for T being TargetCat of I
for D being Categorial Category
for F being Functor of T,D
for J being Indexing of D holds (J * F) * I = J * (F * I)
let I be Indexing of C; for T being TargetCat of I
for D being Categorial Category
for F being Functor of T,D
for J being Indexing of D holds (J * F) * I = J * (F * I)
let T be TargetCat of I; for D being Categorial Category
for F being Functor of T,D
for J being Indexing of D holds (J * F) * I = J * (F * I)
let D be Categorial Category; for F being Functor of T,D
for J being Indexing of D holds (J * F) * I = J * (F * I)
let F be Functor of T,D; for J being Indexing of D holds (J * F) * I = J * (F * I)
let J be Indexing of D; (J * F) * I = J * (F * I)
A1:
( F * I = (F * (I -functor (C,T))) -indexing_of C & Image (F * (I -functor (C,T))) is Subcategory of D )
by Def17;
D is TargetCat of F * I
by Th29;
then
rng (F * I) is Subcategory of D
by Th14;
then A2:
Image ((F * I) -functor (C,(rng (F * I)))) is Subcategory of D
by CAT_5:4;
thus (J * F) * I =
(J * F) * (I -functor (C,T))
by Th32
.=
J * (F * (I -functor (C,T)))
by Th26
.=
J * (F * I)
by A1, A2, Th18, Th22
; verum