let C, D be Category; :: thesis: 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; :: thesis: for d being Object of D holds (Obj (pr2 C,D)) . c,d = d
let d be Object of D; :: thesis: (Obj (pr2 C,D)) . c,d = d
A1: id [c,d] = [(id c),(id d)] by Th41;
(pr2 C,D) . (id c),(id d) = id d by FUNCT_3:def 6;
hence (Obj (pr2 C,D)) . c,d = d by A1, CAT_1:103; :: thesis: verum