reconsider zeroseq = NAT --> 0c as Complex_Sequence ;
A1: for n being Element of NAT holds zeroseq . n = 0c by FUNCOP_1:7;
A2: zeroseq in the_set_of_ComplexSequences by Def1;
then seq_id zeroseq = zeroseq by Def2;
hence ex b₁ being Element of the_set_of_ComplexSequences st
for n being Element of NAT holds (seq_id b₁) . n = 0c by A1, A2; :: thesis: verum