theorem T4: :: RING_4:18

for R being Ring
for a, b being Element of R holds (a | R) *' (b | R) = (a * b) | R