theorem Th3: :: HEINE:3

for seq being Real_Sequence st seq is divergent_to+infty holds
2 to_power seq is divergent_to+infty