deffunc H₁( Element of NAT , Element of NAT ) -> Element of REAL = ((a rExpSeq ) . $2) * (((Partial_Sums (b rExpSeq )) . $1) - ((Partial_Sums (b rExpSeq )) . ($1 -' $2)));
for n being Element of NAT ex rseq being Real_Sequence st
for k being Element of 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 Element of 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