let e1, e2 be FinSequence of ExtREAL ; :: thesis:
assume that
A2: len e1 = len e and
A3: for k being Nat st k in dom e1 holds
e1 . k = Sum (e . k) and
A4: len e2 = len e and
A5: for k being Nat st k in dom e2 holds
e2 . k = Sum (e . k) ; :: thesis:
( dom e1 = dom e2 & ( for k being Nat st k in dom e1 holds
e1 . k = e2 . k ) )

thus A6: dom e1 = Seg (len e) by A2, FINSEQ_1:def 3
.= dom e2 by A4, FINSEQ_1:def 3 ; :: thesis:
let k be Nat; :: thesis:
assume A7: k in dom e1 ; :: thesis:
thus e1 . k = Sum (e . k) by A3, A7
.= e2 . k by A5, A6, A7 ; :: thesis:

end;