let x be Real_Sequence; :: thesis: seq_id x = x
reconsider x1 = x as set ;
x1 in the_set_of_RealSequences by Def1;
hence seq_id x = x by Def2; :: thesis: verum