theorem Th1: :: EC_PF_2:1

for K being Field
for a1, a2 being Element of K st a1 = - a2 holds
a1 |^ 2 = a2 |^ 2