scheme :: SEQ_1:sch 1
ExRealSeq{ F1( object ) -> Real } :
ex seq being Real_Sequence st
for n being Nat holds seq . n = F1(n)