let C be Category; :: thesis: for I being Indexing of C
for D being TargetCat of I
for J being Indexing of D
for E being TargetCat of J
for K being Indexing of E holds (K * J) * I = K * (J * I)
let I be Indexing of C; :: thesis: for D being TargetCat of I
for J being Indexing of D
for E being TargetCat of J
for K being Indexing of E holds (K * J) * I = K * (J * I)
let D be TargetCat of I; :: thesis: for J being Indexing of D
for E being TargetCat of J
for K being Indexing of E holds (K * J) * I = K * (J * I)
let J be Indexing of D; :: thesis: for E being TargetCat of J
for K being Indexing of E holds (K * J) * I = K * (J * I)
let E be TargetCat of J; :: thesis: for K being Indexing of E holds (K * J) * I = K * (J * I)
let K be Indexing of E; :: thesis: (K * J) * I = K * (J * I)
thus (K * J) * I = (K * J) * (I -functor (C,D)) by Th32
.= K * (J * (I -functor (C,D))) by Th37
.= K * (J * I) by Th32 ; :: thesis: verum