let n be Nat; :: thesis: ((n + 2) * ((2 * (n + 1)) + 1)) * ((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - (3 * (n + 1))) + 1) = ((((((6 * (n |^ 6)) + (57 * (n |^ 5))) + (216 * (n |^ 4))) + (414 * (n |^ 3))) + (419 * (n |^ 2))) + (211 * n)) + 42
((n + 2) * ((2 * (n + 1)) + 1)) * ((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - (3 * (n + 1))) + 1) = ((n + 2) * ((2 * n) + 3)) * ((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - (3 * n)) - 2)
.= ((n + 2) * ((2 * n) + 3)) * ((((3 * (((((n |^ 4) + (4 * (n |^ 3))) + (6 * (n |^ 2))) + (4 * n)) + 1)) + (6 * ((n + 1) |^ 3))) - (3 * n)) - 2) by Lm6
.= ((n + 2) * ((2 * n) + 3)) * ((((((((3 * (n |^ 4)) + (12 * (n |^ 3))) + (18 * (n |^ 2))) + (12 * n)) + 3) + (6 * ((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1))) - (3 * n)) - 2) by Lm4
.= (((2 * (n * n)) + (3 * n)) + ((4 * n) + 6)) * (((((3 * (n |^ 4)) + (18 * (n |^ 3))) + (36 * (n |^ 2))) + (27 * n)) + 7)
.= (((2 * (n |^ 2)) + (3 * n)) + ((4 * n) + 6)) * (((((3 * (n |^ 4)) + (18 * (n |^ 3))) + (36 * (n |^ 2))) + (27 * n)) + 7) by WSIERP_1:1
.= (((((3 * (n |^ 4)) * (((2 * (n |^ 2)) + (7 * n)) + 6)) + ((18 * (n |^ 3)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((36 * (n |^ 2)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((((27 * (n * (n |^ 2))) * 2) + ((27 * (n * n)) * 7)) + (162 * n))) + (((14 * (n |^ 2)) + (49 * n)) + 42)
.= (((((3 * (n |^ 4)) * (((2 * (n |^ 2)) + (7 * n)) + 6)) + ((18 * (n |^ 3)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((36 * (n |^ 2)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((((27 * (n |^ (2 + 1))) * 2) + ((27 * (n * n)) * 7)) + (162 * n))) + (((14 * (n |^ 2)) + (49 * n)) + 42) by NEWTON:6
.= (((((3 * (n |^ 4)) * (((2 * (n |^ 2)) + (7 * n)) + 6)) + ((18 * (n |^ 3)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((36 * (n |^ 2)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + (((54 * (n |^ 3)) + ((27 * (n |^ 2)) * 7)) + (162 * n))) + (((14 * (n |^ 2)) + (49 * n)) + 42) by WSIERP_1:1
.= ((((((3 * ((n |^ 4) * (n |^ 2))) * 2) + ((3 * ((n |^ 4) * n)) * 7)) + (18 * (n |^ 4))) + ((((18 * ((n |^ 3) * (n |^ 2))) * 2) + ((18 * ((n |^ 3) * n)) * 7)) + (108 * (n |^ 3)))) + ((36 * (n |^ 2)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42)
.= ((((((3 * (n |^ (4 + 2))) * 2) + ((3 * ((n |^ 4) * n)) * 7)) + (18 * (n |^ 4))) + ((((18 * ((n |^ 3) * (n |^ 2))) * 2) + ((18 * ((n |^ 3) * n)) * 7)) + (108 * (n |^ 3)))) + ((36 * (n |^ 2)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42) by NEWTON:8
.= (((((6 * (n |^ (4 + 2))) + ((3 * (n |^ (4 + 1))) * 7)) + (18 * (n |^ 4))) + (((36 * ((n |^ 3) * (n |^ 2))) + (126 * ((n |^ 3) * n))) + (108 * (n |^ 3)))) + ((36 * (n |^ 2)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42) by NEWTON:6
.= (((((6 * (n |^ (4 + 2))) + (21 * (n |^ (4 + 1)))) + (18 * (n |^ 4))) + (((36 * ((n |^ 3) * (n |^ 2))) + (126 * (n |^ (3 + 1)))) + (108 * (n |^ 3)))) + ((36 * (n |^ 2)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42) by NEWTON:6
.= (((((6 * (n |^ (4 + 2))) + (21 * (n |^ (4 + 1)))) + (18 * (n |^ 4))) + (((36 * (n |^ (3 + 2))) + (126 * (n |^ (3 + 1)))) + (108 * (n |^ 3)))) + ((36 * (n |^ 2)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42) by NEWTON:8
.= (((((6 * (n |^ 6)) + (21 * (n |^ 5))) + (18 * (n |^ 4))) + (((36 * (n |^ 5)) + (126 * (n |^ 4))) + (108 * (n |^ 3)))) + ((((36 * ((n |^ 2) * (n |^ 2))) * 2) + ((36 * ((n |^ 2) * n)) * 7)) + (216 * (n |^ 2)))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42)
.= (((((6 * (n |^ 6)) + (21 * (n |^ 5))) + (18 * (n |^ 4))) + (((36 * (n |^ 5)) + (126 * (n |^ 4))) + (108 * (n |^ 3)))) + ((((36 * (n |^ (2 + 2))) * 2) + (252 * ((n |^ 2) * n))) + (216 * (n |^ 2)))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42) by NEWTON:8
.= (((((6 * (n |^ 6)) + (21 * (n |^ 5))) + (18 * (n |^ 4))) + (((36 * (n |^ 5)) + (126 * (n |^ 4))) + (108 * (n |^ 3)))) + (((72 * (n |^ (2 + 2))) + (252 * (n |^ (2 + 1)))) + (216 * (n |^ 2)))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42) by NEWTON:6
.= (((((6 * (n |^ 6)) + (21 * (n |^ 5))) + (18 * (n |^ 4))) + (((36 * (n |^ 5)) + (126 * (n |^ 4))) + (108 * (n |^ 3)))) + (((72 * (n |^ 4)) + (252 * (n |^ 3))) + (216 * (n |^ 2)))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42) ;
hence ((n + 2) * ((2 * (n + 1)) + 1)) * ((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - (3 * (n + 1))) + 1) = ((((((6 * (n |^ 6)) + (57 * (n |^ 5))) + (216 * (n |^ 4))) + (414 * (n |^ 3))) + (419 * (n |^ 2))) + (211 * n)) + 42 ; :: thesis: verum