let x1, x2 be Element of REAL n; :: thesis: ( dom x1 = Seg n & ( for i being Element of NAT st i in Seg n holds
x1 . i = integral ((proj i,n) * f),A ) & dom x2 = Seg n & ( for i being Element of NAT st i in Seg n holds
x2 . i = integral ((proj i,n) * f),A ) implies x1 = x2 )
assume that
A5: dom x1 = Seg n and
A6: for i being Element of NAT st i in Seg n holds
x1 . i = integral ((proj i,n) * f),A and
A7: dom x2 = Seg n and
A8: for i being Element of NAT st i in Seg n holds
x2 . i = integral ((proj i,n) * f),A ; :: thesis: x1 = x2
for k being Nat st k in dom x1 holds
x1 . k = x2 . k

proof

let k be Nat; :: thesis: ( k in dom x1 implies x1 . k = x2 . k )
assume A9: k in dom x1 ; :: thesis: x1 . k = x2 . k
then reconsider k = k as Element of NAT ;
x2 . k = integral ((proj k,n) * f),A by A5, A8, A9;
hence x1 . k = x2 . k by A5, A6, A9; :: thesis: verum

end;

hence x1 = x2 by A5, A7, FINSEQ_1:17; :: thesis: verum