deffunc H₁( Nat) -> Element of K21(K22(D,REAL)) = (H . $1) ^ ;
thus ex f being Functional_Sequence of D,REAL st
for n being Nat holds f . n = H₁(n) from SEQFUNC:sch 1(); :: thesis: verum