theorem :: SEQ_1:27

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