theorem Th25: :: TOPGEN_3:25

for X being set
for n being Element of NAT holds Sum ((X -powers (1 / 2)) ^\ (n + 1)) <= (1 / 2) |^ n