let C be Category; :: thesis: for I being Indexing of C
for T1 being TargetCat of I
for J being Indexing of T1
for T2 being TargetCat of J
for D being Categorial Category
for F being Functor of T2,D holds (F * J) * I = F * (J * I)
let I be Indexing of C; :: thesis: for T1 being TargetCat of I
for J being Indexing of T1
for T2 being TargetCat of J
for D being Categorial Category
for F being Functor of T2,D holds (F * J) * I = F * (J * I)
let T1 be TargetCat of I; :: thesis: for J being Indexing of T1
for T2 being TargetCat of J
for D being Categorial Category
for F being Functor of T2,D holds (F * J) * I = F * (J * I)
let J be Indexing of T1; :: thesis: for T2 being TargetCat of J
for D being Categorial Category
for F being Functor of T2,D holds (F * J) * I = F * (J * I)
let T2 be TargetCat of J; :: thesis: for D being Categorial Category
for F being Functor of T2,D holds (F * J) * I = F * (J * I)
let D be Categorial Category; :: thesis: for F being Functor of T2,D holds (F * J) * I = F * (J * I)
let F be Functor of T2,D; :: thesis: (F * J) * I = F * (J * I)
thus (F * J) * I = (F * J) * (I -functor (C,T1)) by Th32
.= F * (J * (I -functor (C,T1))) by Th34
.= F * (J * I) by Th32 ; :: thesis: verum