deffunc H₁( Nat) -> Element of REAL = In (((lower_bound (rng (f | (divset (D,$1))))) * (vol (divset (D,$1)))),REAL);
consider IT being FinSequence of REAL such that
A9: ( 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 A9; :: 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))) )
A10: In (((lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))),REAL) = (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 A9, FINSEQ_3:29;
hence IT . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A9, A10; :: thesis: verum