deffunc H₁( Nat) -> Real = middle_sum (f,(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 Element of NAT holds IT . i = middle_sum (f,(S . i))
let i be Element of NAT ; :: thesis: IT . i = middle_sum (f,(S . i))
IT . i = H₁(i) by A1;
hence IT . i = middle_sum (f,(S . i)) ; :: thesis: verum