deffunc H₁( Element of NAT ) -> Element of REAL n = middle_sum f,(S . $1);
A1: REAL n = the carrier of (REAL-NS n) by REAL_NS1:def 4;
ex IT being sequence of (REAL n) st
for i being Element of NAT holds IT . i = H₁(i) from FUNCT_2:sch 4();
hence ex b₁ being sequence of (REAL-NS n) st
for i being Element of NAT holds b₁ . i = middle_sum f,(S . i) by A1; :: thesis: verum