theorem Th4: :: MODCAT_1:4

for R being Ring
for x, y1, y2 being object st GO x,y1,R & GO x,y2,R holds
y1 = y2