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:96 ; :: thesis: verum