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