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)
reconsider T9 = T as TargetCat of I * F by Th24;
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)
reconsider G9 = G as Functor of T9,E ;
reconsider GI = rng (G * I) as TargetCat of (G * (I -functor (D,T))) -indexing_of D by Def17;
A1: I * F = ((I -functor (D,T)) * F) -indexing_of C by Th23;
A2: ((G * (I -functor (D,T))) -indexing_of D) -functor (D,GI) = G * (I -functor (D,T)) by Th18;
( G * I = (G * (I -functor (D,T))) -indexing_of D & Image F is Subcategory of D ) by Def17;
hence (G * I) * F = ((((G * (I -functor (D,T))) -indexing_of D) -functor (D,GI)) * F) -indexing_of C by Def16
.= ((G * (I -functor (D,T))) * F) -indexing_of C by A2, Th2
.= (G * ((I -functor (D,T)) * F)) -indexing_of C by RELAT_1:36
.= (G9 * ((I * F) -functor (C,T9))) -indexing_of C by A1, Th18
.= G * (I * F) by Def17 ;
:: thesis: verum