let C be Category; :: thesis: for I being Indexing of C
for T being TargetCat of I holds pr2 (I -functor (C,T)) = I `2
let I be Indexing of C; :: thesis: for T being TargetCat of I holds pr2 (I -functor (C,T)) = I `2
let T be TargetCat of I; :: thesis: pr2 (I -functor (C,T)) = I `2
A1: dom (I -functor (C,T)) = the carrier' of C by FUNCT_2:def 1;

A2: now :: thesis: for x being object st x in the carrier' of C holds
(pr2 (I -functor (C,T))) . x = (I `2) . x

let x be object ; :: thesis: ( x in the carrier' of C implies (pr2 (I -functor (C,T))) . x = (I `2) . x )
assume x in the carrier' of C ; :: thesis: (pr2 (I -functor (C,T))) . x = (I `2) . x
then reconsider f = x as Morphism of C ;
(I -functor (C,T)) . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] by Def11;
then ((I -functor (C,T)) . x) `2 = (I `2) . f ;
hence (pr2 (I -functor (C,T))) . x = (I `2) . x by A1, MCART_1:def 13; :: thesis: verum

end;

( dom (pr2 (I -functor (C,T))) = dom (I -functor (C,T)) & dom (I `2) = the carrier' of C ) by MCART_1:def 13, PARTFUN1:def 2;
hence pr2 (I -functor (C,T)) = I `2 by A1, A2; :: thesis: verum