scheme :: SIN_COS:sch 2
ExRealCASE{ F1( Nat, Nat) -> Real } :
for k being Nat ex rseq being Real_Sequence st
for n being Nat holds
( ( n <= k implies rseq . n = F1(k,n) ) & ( n > k implies rseq . n = 0 ) )