scheme :: COMSEQ_1:sch 1
ExComplexSeq{ F1( set ) -> Complex } :
ex seq being Complex_Sequence st
for n being Nat holds seq . n = F1(n)