deffunc H_{1}( 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_{1}(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_{1}(i)
by A1;

hence IT . i = middle_sum (f,(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 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

hence IT . i = middle_sum (f,(S . i)) ; :: thesis: verum