theorem :: RING_5:3

for R being Ring
for a being Element of R holds a |^ 2 = a * a by prl4;