deffunc H₁( Nat, Nat) -> Element of REAL = ((a rExpSeq) . $2) * (((Partial_Sums (b rExpSeq)) . $1) - ((Partial_Sums (b rExpSeq)) . ($1 -' $2)));
for n being Nat ex rseq being Real_Sequence st
for k being Nat holds
( ( k <= n implies rseq . k = H₁(n,k) ) & ( k > n implies rseq . k = 0 ) ) from SIN_COS:sch 2();
hence ex b₁ being Real_Sequence st
for k being Nat holds
( ( k <= n implies b₁ . k = ((a rExpSeq) . k) * (((Partial_Sums (b rExpSeq)) . n) - ((Partial_Sums (b rExpSeq)) . (n -' k))) ) & ( n < k implies b₁ . k = 0 ) ) ; :: thesis: verum