for n being Nat holds (NAT --> 0c) . n = 0c by ORDINAL1:def 12, FUNCOP_1:7;
hence ex b₁ being Complex_Sequence st b₁ is convergent by Th9; :: thesis: verum