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