let C be Category; :: thesis: for I being Indexing of C
for T being TargetCat of I holds (I -functor C,T) -indexing_of C = I
let I be Indexing of C; :: thesis: for T being TargetCat of I holds (I -functor C,T) -indexing_of C = I
let T be TargetCat of I; :: thesis: (I -functor C,T) -indexing_of C = I
set F = I -functor C,T;
A1: ex f being ManySortedSet of the carrier of C ex g being ManySortedSet of the carrier' of C st I = [f,g] by Def4;
thus (I -functor C,T) -indexing_of C = [(I `1 ),(pr2 (I -functor C,T))] by Lm2
.= [(I `1 ),(I `2 )] by Th20
.= I by A1, MCART_1:8 ; :: thesis: verum