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