let s1, s2 be FinSequence of REAL ; ( len s1 = len D & ( for i being Nat st i in dom D holds
s1 . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) & len s2 = len D & ( for i being Nat st i in dom D holds
s2 . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) implies s1 = s2 )
assume that
A11:
len s1 = len D
and
A12:
for i being Nat st i in dom D holds
s1 . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))
and
A13:
len s2 = len D
and
A14:
for i being Nat st i in dom D holds
s2 . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))
; s1 = s2
A15:
dom s1 = dom D
by A11, FINSEQ_3:29;
for i being Nat st i in dom s1 holds
s1 . i = s2 . i
hence
s1 = s2
by A11, A13, FINSEQ_2:9; verum