x in the_set_of_RealSequences by Def8;
hence seq_id x = x by Def2; :: thesis: verum