x in the_set_of_ComplexSequences by FUNCT_2:8;
hence seq_id x = x by Def2; :: thesis: verum