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