let a, b, c be Real; ((a + b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c)
((a + b) + c) |^ (1 + 1) =
(((a + b) + c) |^ 1) * ((a + b) + c)
by NEWTON:6
.=
((a + b) + c) * ((a + b) + c)
.=
((((a * a) + (a * b)) + (a * c)) + (((a * b) + (b * b)) + (b * c))) + (((a * c) + (c * b)) + (c * c))
.=
((((a * a) + (a * b)) + (a * c)) + (((a * b) + (b |^ 2)) + (b * c))) + (((a * c) + (c * b)) + (c * c))
by WSIERP_1:1
.=
((((a |^ 2) + (a * b)) + (a * c)) + (((a * b) + (b |^ 2)) + (b * c))) + (((a * c) + (c * b)) + (c * c))
by WSIERP_1:1
.=
((((a |^ 2) + (a * b)) + (a * c)) + (((a * b) + (b |^ 2)) + (b * c))) + (((a * c) + (c * b)) + (c |^ 2))
by WSIERP_1:1
.=
(((((a |^ 2) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c)) + (b |^ 2)
;
hence
((a + b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c)
; verum