theorem P4: :: REALALG2:8

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