let C be Category; :: thesis: for D being Categorial Category
for I1 being Indexing of C
for I2 being Indexing of D
for T being TargetCat of I2 st D is TargetCat of I1 holds
I2 * I1 = (I2 -functor D,T) * I1
let D be Categorial Category; :: thesis: for I1 being Indexing of C
for I2 being Indexing of D
for T being TargetCat of I2 st D is TargetCat of I1 holds
I2 * I1 = (I2 -functor D,T) * I1
let I1 be Indexing of C; :: thesis: for I2 being Indexing of D
for T being TargetCat of I2 st D is TargetCat of I1 holds
I2 * I1 = (I2 -functor D,T) * I1
let I2 be Indexing of D; :: thesis: for T being TargetCat of I2 st D is TargetCat of I1 holds
I2 * I1 = (I2 -functor D,T) * I1
let T be TargetCat of I2; :: thesis: ( D is TargetCat of I1 implies I2 * I1 = (I2 -functor D,T) * I1 )
assume D is TargetCat of I1 ; :: thesis: I2 * I1 = (I2 -functor D,T) * I1
then reconsider D' = D as TargetCat of I1 ;
reconsider I2' = I2 as Indexing of D' ;
reconsider T' = T as TargetCat of I2' ;
( Image (I1 -functor C,D') = rng I1 & Image (I1 -functor C,(rng I1)) = rng I1 ) by Def12;
hence I2 * I1 = I2 * (I1 -functor C,D') by Th11, Th22
.= ((I2' -functor D',T') * (I1 -functor C,D')) -indexing_of C by Th23
.= (I2 -functor D,T) * I1 by Def17 ;
:: thesis: verum