for x being Real_Sequence holds seq_id x = x ;