let n be Nat; :: thesis: (n + 2) * ((((n + 1) |^ 2) + (n + 1)) - 1) = (((n |^ 3) + (5 * (n |^ 2))) + (7 * n)) + 2
(n + 2) * ((((n + 1) |^ 2) + (n + 1)) - 1) = (n + 2) * (((((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2)) + (n + 1)) - 1) by Lm3
.= (n + 2) * (((((n |^ 2) + ((2 * n) * 1)) + 1) + (n + 1)) - 1)
.= (((((n * (n |^ 2)) + (2 * (n |^ 2))) + (3 * (n * n))) + (6 * n)) + n) + 2
.= (((((n * (n |^ 2)) + (2 * (n |^ 2))) + (3 * (n |^ 2))) + (6 * n)) + n) + 2 by WSIERP_1:1
.= (((((n |^ (2 + 1)) + (2 * (n |^ 2))) + (3 * (n |^ 2))) + (6 * n)) + n) + 2 by NEWTON:6
.= (((n |^ (2 + 1)) + ((2 + 3) * (n |^ 2))) + ((6 + 1) * n)) + 2 ;
hence (n + 2) * ((((n + 1) |^ 2) + (n + 1)) - 1) = (((n |^ 3) + (5 * (n |^ 2))) + (7 * n)) + 2 ; :: thesis: verum