A1: h is non-zero by Def1;
A2: h is convergent by Def1;
lim h = 0 by Def1;
then lim (h ^\ n) = 0 by A2, SEQ_4:33;
hence h ^\ n is convergent_to_0 by A1, A2, Def1; :: thesis: verum