deffunc H₁( Element of NAT ) -> Point of X = middle_sum (f,(S . $1));
thus ex IT being sequence of the carrier of X st
for i being Element of NAT holds IT . i = H₁(i) from FUNCT_2:sch 4(); :: thesis: verum