deffunc H₁( Element of NAT ) -> Element of REAL = lower_sum (f,(T . $1));
thus ex IT being Real_Sequence st
for i being Element of NAT holds IT . i = H₁(i) from SEQ_1:sch 1(); :: thesis: verum