h is non-zero by Def4;
then A1: h ^\ n is non-zero by Th17;
A2: h is convergent by Def4;
lim h = 0. S by Def4;
then A3: lim (h ^\ n) = 0. S by A2, LOPBAN_3:9;
h ^\ n is convergent by A2, LOPBAN_3:9;
hence for b₁ being sequence of S st b₁ = h ^\ n holds
b₁ is convergent_to_0 by A1, A3, Def4; :: thesis: verum