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:31;
hence IT . i = (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) by A8; :: thesis: verum