deffunc H1( 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 = H1(i) ) )
from FINSEQ_2:sch 1();
take
IT
; ( 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; 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; ( i in dom D implies IT . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) )
A2:
H1(i) = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))
;
assume
i in dom D
; 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; verum