theorem P3: :: REALALG2:7

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