deffunc H₁( Nat) -> Element of REAL = (lower_bound (rng (f | (divset (D,$1))))) * (vol (divset (D,$1)));
consider IT being FinSequence of REAL such that
A8: ( len IT = len D & ( for i being Nat st i in dom IT holds
IT . i = H₁(i) ) ) from FINSEQ_2:sch 1();
take IT ; :: thesis: ( len IT = len D & ( for i being Nat st i in dom D holds
IT . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) )
thus len IT = len D by A8; :: thesis: for i being Nat st i in dom D holds
IT . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))
let i be Nat; :: thesis: ( i in dom D implies IT . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) )
assume i in dom D ; :: thesis: IT . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))
then i in dom IT by A8, FINSEQ_3:29;
hence IT . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A8; :: thesis: verum