let s1, s2 be FinSequence of REAL ; :: thesis: ( len s1 = len TD & ( for i being Nat st i in dom TD holds
s1 . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) & len s2 = len TD & ( for i being Nat st i in dom TD holds
s2 . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) implies s1 = s2 )
assume that
A3: len s1 = len TD and
A4: for i being Nat st i in dom TD holds
s1 . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) and
A5: len s2 = len TD and
A6: for i being Nat st i in dom TD holds
s2 . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ; :: thesis: s1 = s2
A7: dom s1 = dom TD by A3, 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 A8: i in dom s1 ; :: thesis: s1 . i = s2 . i
then s1 . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) by A4, A7;
hence s1 . i = s2 . i by A6, A7, A8; :: thesis: verum

end;

hence s1 = s2 by A3, A5, FINSEQ_2:9; :: thesis: verum