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

proof

thus A5: dom e1 = Seg (len e) by A3, FINSEQ_1:def 3
.= dom e2 by A4, FINSEQ_1:def 3 ; :: thesis: for k being Nat st k in dom e1 holds
e1 . k = e2 . k
let k be Nat; :: thesis: ( k in dom e1 implies e1 . k = e2 . k )
assume A6: k in dom e1 ; :: thesis: e1 . k = e2 . k
thus e1 . k = Sum (e . k) by A3, A6
.= e2 . k by A4, A5, A6 ; :: thesis: verum

end;

hence e1 = e2 by FINSEQ_1:17; :: thesis: verum