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