let x1, x2 be Element of REAL n; :: thesis:
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),A) 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),A) ; :: thesis:
for k being Nat st k in dom x1 holds
x1 . k = x2 . k

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

end;