let s1, s2 be FinSequence of REAL ; :: thesis: ( 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))) ; :: thesis: 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

proof

let i be Nat; :: thesis: ( i in dom s1 implies s1 . i = s2 . i )
assume A16: i in dom s1 ; :: thesis: s1 . i = s2 . i
then s1 . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A12, A15;
hence s1 . i = s2 . i by A14, A15, A16; :: thesis: verum

end;

hence s1 = s2 by A11, A13, FINSEQ_2:9; :: thesis: verum