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