theorem :: CSSPACE:1

for x being Complex_Sequence holds seq_id x = x ;