deffunc H₁( Nat) -> Point of X = middle_sum (f,(S . $1));
consider IT being sequence of the carrier of X such that
A1: for i being Element of NAT holds IT . i = H₁(i) from FUNCT_2:sch 4();
take IT ; :: thesis: for i being Nat holds IT . i = middle_sum (f,(S . i))
let n be Nat; :: thesis: IT . n = middle_sum (f,(S . n))
n in NAT by ORDINAL1:def 12;
hence IT . n = middle_sum (f,(S . n)) by A1; :: thesis: verum