let C, D be Category; :: thesis: for c being Object of
for d being Object of holds id [c,d] = [(id c),(id d)]
let c be Object of ; :: thesis: for d being Object of holds id [c,d] = [(id c),(id d)]
let d be Object of ; :: 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