theorem sq00: :: REALALG2:10

for R being domRing
for a, b being Element of R holds
( a ^2 = b ^2 iff ( a = b or a = - b ) )