:: deftheorem Def12 defines Sequence-yielding DIFF_1:def 12 :
for S being Functional_Sequence of REAL,REAL holds
( S is Sequence-yielding iff for n being Nat holds S . n is Real_Sequence );