let C, D be Category; for c being Object of C
for d being Object of D holds (Obj (pr2 (C,D))) . (c,d) = d
let c be Object of C; for d being Object of D holds (Obj (pr2 (C,D))) . (c,d) = d
let d be Object of D; (Obj (pr2 (C,D))) . (c,d) = d
( id [c,d] = [(id c),(id d)] & (pr2 (C,D)) . ((id c),(id d)) = id d )
by Th25, FUNCT_3:def 5;
hence
(Obj (pr2 (C,D))) . (c,d) = d
by CAT_1:67; verum