scheme :: COMSEQ_1:sch 1
ExComplexSeq{ F₁( set ) -> Complex } :

ex seq being Complex_Sequence st
for n being Nat holds seq . n = F₁(n)