theorem :: COMSEQ_1:21

for seq being Complex_Sequence holds 1r (#) seq = seq