deffunc H₁( Nat) -> object = Sum (S . (In ($1,NAT)));
consider IT being Real_Sequence such that
A1: for i being Nat holds IT . i = H₁(i) from SEQ_1:sch 1();
take IT ; :: thesis: for i being Nat holds IT . i = Sum (S . i)
let i be Nat; :: thesis: IT . i = Sum (S . i)
IT . i = H₁(i) by A1;
hence IT . i = Sum (S . i) ; :: thesis: verum