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