let C be Category; 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; 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; 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; 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; ( D is TargetCat of I1 implies I2 * I1 = (I2 -functor (D,T)) * I1 )
assume
D is TargetCat of I1
; I2 * I1 = (I2 -functor (D,T)) * I1
then reconsider D9 = D as TargetCat of I1 ;
reconsider I29 = I2 as Indexing of D9 ;
reconsider T9 = T as TargetCat of I29 ;
( Image (I1 -functor (C,D9)) = rng I1 & Image (I1 -functor (C,(rng I1))) = rng I1 )
by Def12;
hence I2 * I1 =
I2 * (I1 -functor (C,D9))
by Th11, Th22
.=
((I29 -functor (D9,T9)) * (I1 -functor (C,D9))) -indexing_of C
by Th23
.=
(I2 -functor (D,T)) * I1
by Def17
;
verum