let x be Complex_Sequence; :: thesis: seq_id x = x
x in the_set_of_ComplexSequences by Def1;
hence seq_id x = x by Def2; :: thesis: verum