deffunc H₁( Nat) -> Element of K19(K20(X,ExtREAL)) = r (#) (F . $1);
thus ex f being Functional_Sequence of X,ExtREAL st
for n being Nat holds f . n = H₁(n) from SEQFUNC:sch 1(); :: thesis: verum