let C, D, E be Category; :: thesis: for F being Functor of C,D
for G being Functor of D,E
for I being Indexing of E holds (I * G) * F = I * (G * F)
let F be Functor of C,D; :: thesis: for G being Functor of D,E
for I being Indexing of E holds (I * G) * F = I * (G * F)
let G be Functor of D,E; :: thesis: for I being Indexing of E holds (I * G) * F = I * (G * F)
let I be Indexing of E; :: thesis: (I * G) * F = I * (G * F)
set T = rng I;
reconsider T9 = rng I as TargetCat of I * G by Th24;
I * G = ((I -functor (E,(rng I))) * G) -indexing_of D by Th23;
then (I * G) -functor (D,T9) = (I -functor (E,(rng I))) * G by Th18;
hence (I * G) * F = (((I -functor (E,(rng I))) * G) * F) -indexing_of C by Th23
.= ((I -functor (E,(rng I))) * (G * F)) -indexing_of C by RELAT_1:36
.= I * (G * F) by Th23 ;
:: thesis: verum