deffunc H_{1}( Nat) -> object = Sum (S . (In ($1,NAT)));

consider IT being Real_Sequence such that

A1: for i being Nat holds IT . i = H_{1}(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_{1}(i)
by A1;

hence IT . i = Sum (S . i) ; :: thesis: verum

consider IT being Real_Sequence such that

A1: for i being Nat holds IT . i = H

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

hence IT . i = Sum (S . i) ; :: thesis: verum