theorem Th1: :: SERIES_4:1

for a, b, c being Real holds ((a + b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c)