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