deffunc H_{1}( Nat) -> object = upper_sum (f,(T . (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 Nat holds IT . i = upper_sum (f,(T . i))

let i be Nat; :: thesis: IT . i = upper_sum (f,(T . i))

IT . i = H_{1}(i)
by A1;

hence IT . i = upper_sum (f,(T . 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 Nat holds IT . i = upper_sum (f,(T . i))

let i be Nat; :: thesis: IT . i = upper_sum (f,(T . i))

IT . i = H

hence IT . i = upper_sum (f,(T . i)) ; :: thesis: verum