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 I1 st D is TargetCat of I1 holds
I2 * I1 = I2 * (I1 -functor (C,T))
let D be Categorial Category; :: thesis: for I1 being Indexing of C
for I2 being Indexing of D
for T being TargetCat of I1 st D is TargetCat of I1 holds
I2 * I1 = I2 * (I1 -functor (C,T))
let I1 be Indexing of C; :: thesis: for I2 being Indexing of D
for T being TargetCat of I1 st D is TargetCat of I1 holds
I2 * I1 = I2 * (I1 -functor (C,T))
let I2 be Indexing of D; :: thesis: for T being TargetCat of I1 st D is TargetCat of I1 holds
I2 * I1 = I2 * (I1 -functor (C,T))
let T be TargetCat of I1; :: thesis: ( D is TargetCat of I1 implies I2 * I1 = I2 * (I1 -functor (C,T)) )
assume D is TargetCat of I1 ; :: thesis: I2 * I1 = I2 * (I1 -functor (C,T))
then reconsider D9 = D as TargetCat of I1 ;
A1: Image (I1 -functor (C,(rng I1))) = rng I1 by Def12;
( Image (I1 -functor (C,D9)) = rng I1 & Image (I1 -functor (C,T)) = rng I1 ) by Def12;
hence I2 * I1 = I2 * (I1 -functor (C,T)) by A1, Th11, Th22; :: thesis: verum