let s1, s2 be FinSequence of REAL ; :: thesis: ( len s1 = len D & ( for i being Nat st i in dom D holds
s1 . i = (upper_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 = (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) implies s1 = s2 )
assume that
A2: ( len s1 = len D & ( for i being Nat st i in dom D holds
s1 . i = (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) ) and
A3: ( len s2 = len D & ( for i being Nat st i in dom D holds
s2 . i = (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) ) ; :: thesis: s1 = s2
Y: ( dom s1 = dom D & dom s2 = dom D ) by A2, A3, FINSEQ_3:31;
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 A4: i in dom s1 ; :: thesis: s1 . i = s2 . i
then s1 . i = (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) by A2, Y;
hence s1 . i = s2 . i by A3, A4, Y; :: thesis: verum

end;

hence s1 = s2 by A2, A3, FINSEQ_2:10; :: thesis: verum