lim h = 0 by Def1;
then A1: lim (h ^\ n) = 0 by CFCONT_1:21;
h ^\ n is convergent by CFCONT_1:21;
hence for b₁ being Complex_Sequence st b₁ = h ^\ n holds
b₁ is convergent_to_0 by A1, Def1; :: thesis: verum