for seq being Real_Sequence holds 1 (#) seq = seq