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