deffunc H₁( Nat, Nat) -> set = (((Coef $1) . $2) * (z |^ $2)) * (w |^ ($1 -' $2));
for n being Nat ex seq being Complex_Sequence st
for k being Nat holds
( ( k <= n implies seq . k = H₁(n,k) ) & ( k > n implies seq . k = 0 ) ) from SIN_COS:sch 1();
hence ex b₁ being Complex_Sequence st
for k being Nat holds
( ( k <= n implies b₁ . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies b₁ . k = 0 ) ) ; :: thesis: verum