let C be Category; :: thesis: for I being Indexing of C
for T being TargetCat of I
for D being Categorial Category
for F being Functor of T,D
for J being Indexing of D holds (J * F) * I = J * (F * I)
let I be Indexing of C; :: thesis: for T being TargetCat of I
for D being Categorial Category
for F being Functor of T,D
for J being Indexing of D holds (J * F) * I = J * (F * I)
let T be TargetCat of I; :: thesis: for D being Categorial Category
for F being Functor of T,D
for J being Indexing of D holds (J * F) * I = J * (F * I)
let D be Categorial Category; :: thesis: for F being Functor of T,D
for J being Indexing of D holds (J * F) * I = J * (F * I)
let F be Functor of T,D; :: thesis: for J being Indexing of D holds (J * F) * I = J * (F * I)
let J be Indexing of D; :: thesis: (J * F) * I = J * (F * I)
A1: ( F * I = (F * (I -functor (C,T))) -indexing_of C & Image (F * (I -functor (C,T))) is Subcategory of D ) by Def17;
D is TargetCat of F * I by Th29;
then rng (F * I) is Subcategory of D by Th14;
then A2: Image ((F * I) -functor (C,(rng (F * I)))) is Subcategory of D by CAT_5:4;
thus (J * F) * I = (J * F) * (I -functor (C,T)) by Th32
.= J * (F * (I -functor (C,T))) by Th26
.= J * (F * I) by A1, A2, Th18, Th22 ; :: thesis: verum