deffunc H_{1}( Nat, Nat) -> Element of the carrier of X = ((z ExpSeq) . $2) * (((Partial_Sums (w ExpSeq)) . $1) - ((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_{1}(n,k) ) & ( k > n implies seq . k = 0. X ) )
from CLOPBAN4:sch 1();

hence ex b_{1} being sequence of X st

for k being Nat holds

( ( k <= n implies b_{1} . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( n < k implies b_{1} . k = 0. X ) )
; :: thesis: verum

for n being Nat ex seq being sequence of X st

for k being Nat holds

( ( k <= n implies seq . k = H

hence ex b

for k being Nat holds

( ( k <= n implies b