let n be Nat; :: thesis: (((n * (4 * (n |^ 2))) + (11 * n)) + (12 * (n |^ 2))) + 3 = (n + 1) * ((4 * ((n + 1) |^ 2)) - 1)
(n + 1) * ((4 * ((n + 1) |^ 2)) - 1) = (n + 1) * ((4 * (((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2))) - 1) by Lm3
.= (n + 1) * ((4 * (((n |^ 2) + (2 * n)) + 1)) - 1)
.= (((n * (4 * (n |^ 2))) + (4 * (n |^ 2))) + ((8 * (n * n)) + (8 * n))) + ((3 * n) + (3 * 1))
.= (((n * (4 * (n |^ 2))) + (4 * (n |^ 2))) + ((8 * (n |^ 2)) + (8 * n))) + ((3 * n) + (3 * 1)) by WSIERP_1:1
.= (((n * (4 * (n |^ 2))) + ((4 * (n |^ 2)) + (8 * (n |^ 2)))) + ((8 * n) + (3 * n))) + 3 ;
hence (((n * (4 * (n |^ 2))) + (11 * n)) + (12 * (n |^ 2))) + 3 = (n + 1) * ((4 * ((n + 1) |^ 2)) - 1) ; :: thesis: verum