deffunc H₁( Element of NAT , Element of NAT ) -> Element of COMPLEX = ((z ExpSeq ) . $2) * ((Partial_Sums (w ExpSeq )) . ($1 -' $2));
A1: for n being Element of NAT ex seq being Complex_Sequence st
for k being Element of NAT holds
( ( k <= n implies seq . k = H₁(n,k) ) & ( k > n implies seq . k = 0 ) ) from SIN_COS:sch 1();
thus ex b₁ being Complex_Sequence st
for k being Element of NAT holds
( ( k <= n implies b₁ . k = ((z ExpSeq ) . k) * ((Partial_Sums (w ExpSeq )) . (n -' k)) ) & ( n < k implies b₁ . k = 0 ) ) by A1; :: thesis: verum