deffunc H₁( Nat, Nat) -> Element of the carrier of X = ((z ExpSeq) . $2) * ((Partial_Sums (w ExpSeq)) . ($1 -' $2));
for n being Nat ex seq being sequence of X st
for k being Nat holds
( ( k <= n implies seq . k = H₁(n,k) ) & ( k > n implies seq . k = 0. X ) ) from CLOPBAN4:sch 1();
hence ex b₁ being sequence of X st
for k being Nat holds
( ( k <= n implies b₁ . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( n < k implies b₁ . k = 0. X ) ) ; :: thesis: verum