let C be Category; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: for G being Functor of D,E holds (G * F) * I = G * (F * I)
let G be Functor of D,E; :: thesis: (G * F) * I = G * (F * I)
reconsider D' = D as TargetCat of F * I by Th29;
reconsider G' = G as Functor of D',E ;
F * I = (F * (I -functor C,T)) -indexing_of C by Def17;
then A1: (F * I) -functor C,D' = F * (I -functor C,T) by Th18;
thus (G * F) * I = ((G * F) * (I -functor C,T)) -indexing_of C by Def17
.= (G' * ((F * I) -functor C,D')) -indexing_of C by A1, RELAT_1:55
.= G * (F * I) by Def17 ; :: thesis: verum