let C, D be Category; :: thesis: for F being Functor of C,D
for I being Indexing of D
for T being TargetCat of I
for E being Categorial Category
for G being Functor of T,E holds (G * I) * F = G * (I * F)
let F be Functor of C,D; :: thesis: for I being Indexing of D
for T being TargetCat of I
for E being Categorial Category
for G being Functor of T,E holds (G * I) * F = G * (I * F)
let I be Indexing of D; :: thesis: for T being TargetCat of I
for E being Categorial Category
for G being Functor of T,E holds (G * I) * F = G * (I * F)
let T be TargetCat of I; :: thesis: for E being Categorial Category
for G being Functor of T,E holds (G * I) * F = G * (I * F)
let E be Categorial Category; :: thesis: for G being Functor of T,E holds (G * I) * F = G * (I * F)
let G be Functor of T,E; :: thesis: (G * I) * F = G * (I * F)
A1: G * I = (G * (I -functor D,T)) -indexing_of D by Def17;
reconsider GI = rng (G * I) as TargetCat of (G * (I -functor D,T)) -indexing_of D by Def17;
A2: I * F = ((I -functor D,T) * F) -indexing_of C by Th23;
reconsider T' = T as TargetCat of I * F by Th24;
reconsider G' = G as Functor of T',E ;
A3: ((G * (I -functor D,T)) -indexing_of D) -functor D,GI = G * (I -functor D,T) by Th18;
Image F is Subcategory of D ;
hence (G * I) * F = ((((G * (I -functor D,T)) -indexing_of D) -functor D,GI) * F) -indexing_of C by A1, Def16
.= ((G * (I -functor D,T)) * F) -indexing_of C by A3, Th2
.= (G * ((I -functor D,T) * F)) -indexing_of C by RELAT_1:55
.= (G' * ((I * F) -functor C,T')) -indexing_of C by A2, Th18
.= G * (I * F) by Def17 ;
:: thesis: verum