theorem Th67: :: CAT_8:67

for C being non empty with_binary_products category
for a, b being Object of C holds (id- a) [x] (id- b) = id- (a [x] b)