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

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: x1 = x2

for k being Nat st k in dom x1 holds

x1 . k = x2 . k

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

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: x1 = x2

for k being Nat st k in dom x1 holds

x1 . k = x2 . k

proof

hence
x1 = x2
by A4, A6, FINSEQ_1:13; :: thesis: verum
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 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: verum

end;assume A8: 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 A4, A7, A8;

hence x1 . k = x2 . k by A4, A5, A8; :: thesis: verum