let C be Category; :: thesis: for I being Indexing of C
for T being TargetCat of I
for D, E being Categorial Category
for F being Functor of T,D
for G being Functor of T,E st F = G holds
F * I = G * I
let I be Indexing of C; :: thesis: for T being TargetCat of I
for D, E being Categorial Category
for F being Functor of T,D
for G being Functor of T,E st F = G holds
F * I = G * I
let T be TargetCat of I; :: thesis: for D, E being Categorial Category
for F being Functor of T,D
for G being Functor of T,E st F = G holds
F * I = G * I
let D, E be Categorial Category; :: thesis: for F being Functor of T,D
for G being Functor of T,E st F = G holds
F * I = G * I
let F be Functor of T,D; :: thesis: for G being Functor of T,E st F = G holds
F * I = G * I
let G be Functor of T,E; :: thesis: ( F = G implies F * I = G * I )
assume A1: F = G ; :: thesis: F * I = G * I
thus F * I = (F * (I -functor (C,T))) -indexing_of C by Def17
.= (G * (I -functor (C,T))) -indexing_of C by A1, Th2
.= G * I by Def17 ; :: thesis: verum