deffunc H₁( Nat) -> Element of REAL = In (((upper_bound (rng (f | (divset (D,$1))))) * (vol (divset (D,$1)))),REAL);
consider IT being FinSequence of REAL such that
A1: ( 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 = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) )
thus len IT = len D by A1; :: thesis: for i being Nat st i in dom D holds
IT . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))
let i be Nat; :: thesis: ( i in dom D implies IT . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) )
A2: H₁(i) = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ;
assume i in dom D ; :: thesis: IT . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))
then i in dom IT by A1, FINSEQ_3:29;
hence IT . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A1, A2; :: thesis: verum