let C be Category; for I being Indexing of C
for T being TargetCat of I
for D, E being Categorial Category
for F being Functor of T,D
for G being Functor of D,E holds (G * F) * I = G * (F * I)
let I be Indexing of C; for T being TargetCat of I
for D, E being Categorial Category
for F being Functor of T,D
for G being Functor of D,E holds (G * F) * I = G * (F * I)
let T be TargetCat of I; for D, E being Categorial Category
for F being Functor of T,D
for G being Functor of D,E holds (G * F) * I = G * (F * I)
let D, E be Categorial Category; for F being Functor of T,D
for G being Functor of D,E holds (G * F) * I = G * (F * I)
let F be Functor of T,D; for G being Functor of D,E holds (G * F) * I = G * (F * I)
reconsider D9 = D as TargetCat of F * I by Th29;
let G be Functor of D,E; (G * F) * I = G * (F * I)
reconsider G9 = G as Functor of D9,E ;
F * I = (F * (I -functor (C,T))) -indexing_of C
by Def17;
then A1:
(F * I) -functor (C,D9) = F * (I -functor (C,T))
by Th18;
thus (G * F) * I =
((G * F) * (I -functor (C,T))) -indexing_of C
by Def17
.=
(G9 * ((F * I) -functor (C,D9))) -indexing_of C
by A1, RELAT_1:36
.=
G * (F * I)
by Def17
; verum