theorem Th47: :: STIRL2_1:47

for n being Nat st n >= 1 holds
n block 2 = (1 / 2) * ((2 |^ n) - 2)