theorem Th15: :: EC_PF_2:15

for K being comRing
for a1, a2 being Element of K holds (a1 + a2) * (a1 - a2) = (a1 |^ 2) - (a2 |^ 2)