theorem P4a: :: REALALG2:9

for R being commutative Ring
for a, b being Element of R holds (a + b) * (a - b) = (a ^2) - (b ^2)