let C, D be Category; :: thesis: for c being Object of C
for d being Object of D holds id [c,d] = [(id c),(id d)]
let c be Object of C; :: thesis: for d being Object of D holds id [c,d] = [(id c),(id d)]
let d be Object of D; :: thesis: id [c,d] = [(id c),(id d)]
thus id [c,d] = [: the Id of C, the Id of D:] . (c,d)
.= [(id c),(id d)] by FUNCT_3:75 ; :: thesis: verum