let x1, x2 be Element of REAL n; :: thesis: ( ( for i being Element of NAT st i in Seg n holds

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & x1 . i = Sum Fi ) ) & ( for i being Element of NAT st i in Seg n holds

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & x2 . i = Sum Fi ) ) implies x1 = x2 )

assume A4: ( ( for i being Element of NAT st i in Seg n holds

ex Fi1 being FinSequence of REAL st

( Fi1 = (proj (i,n)) * F & x1 . i = Sum Fi1 ) ) & ( for i being Element of NAT st i in Seg n holds

ex Fi2 being FinSequence of REAL st

( Fi2 = (proj (i,n)) * F & x2 . i = Sum Fi2 ) ) ) ; :: thesis: x1 = x2

A5: for k0 being Nat st k0 in dom x1 holds

x1 . k0 = x2 . k0

len x1 = n by CARD_1:def 7;

then dom x1 = Seg n by FINSEQ_1:def 3

.= dom x2 by A7, FINSEQ_1:def 3 ;

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

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & x1 . i = Sum Fi ) ) & ( for i being Element of NAT st i in Seg n holds

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & x2 . i = Sum Fi ) ) implies x1 = x2 )

assume A4: ( ( for i being Element of NAT st i in Seg n holds

ex Fi1 being FinSequence of REAL st

( Fi1 = (proj (i,n)) * F & x1 . i = Sum Fi1 ) ) & ( for i being Element of NAT st i in Seg n holds

ex Fi2 being FinSequence of REAL st

( Fi2 = (proj (i,n)) * F & x2 . i = Sum Fi2 ) ) ) ; :: thesis: x1 = x2

A5: for k0 being Nat st k0 in dom x1 holds

x1 . k0 = x2 . k0

proof

A7:
len x2 = n
by CARD_1:def 7;
let k0 be Nat; :: thesis: ( k0 in dom x1 implies x1 . k0 = x2 . k0 )

assume A6: k0 in dom x1 ; :: thesis: x1 . k0 = x2 . k0

then reconsider k = k0 as Element of NAT ;

len x1 = n by CARD_1:def 7;

then k0 in Seg n by A6, FINSEQ_1:def 3;

then ( ex Fi1 being FinSequence of REAL st

( Fi1 = (proj (k,n)) * F & x1 . k = Sum Fi1 ) & ex Fi2 being FinSequence of REAL st

( Fi2 = (proj (k,n)) * F & x2 . k = Sum Fi2 ) ) by A4;

hence x1 . k0 = x2 . k0 ; :: thesis: verum

end;assume A6: k0 in dom x1 ; :: thesis: x1 . k0 = x2 . k0

then reconsider k = k0 as Element of NAT ;

len x1 = n by CARD_1:def 7;

then k0 in Seg n by A6, FINSEQ_1:def 3;

then ( ex Fi1 being FinSequence of REAL st

( Fi1 = (proj (k,n)) * F & x1 . k = Sum Fi1 ) & ex Fi2 being FinSequence of REAL st

( Fi2 = (proj (k,n)) * F & x2 . k = Sum Fi2 ) ) by A4;

hence x1 . k0 = x2 . k0 ; :: thesis: verum

len x1 = n by CARD_1:def 7;

then dom x1 = Seg n by FINSEQ_1:def 3

.= dom x2 by A7, FINSEQ_1:def 3 ;

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