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) ) & dom x2 = Seg n & ( for i being Element of NAT st i in Seg n holds
x2 . i = integral ((proj (i,n)) * f) ) implies x1 = x2 )
assume that
A4: dom x1 = Seg n and
A5: for i being Element of NAT st i in Seg n holds
x1 . i = integral ((proj (i,n)) * f) and
A6: dom x2 = Seg n and
A7: for i being Element of NAT st i in Seg n holds
x2 . i = integral ((proj (i,n)) * f) ; :: thesis: x1 = x2

now :: thesis: for k being Nat st k in dom x1 holds
x1 . k = x2 . k

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

end;

hence x1 = x2 by A4, A6, FINSEQ_1:13; :: thesis: verum