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
proof
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;
A7: len x2 = n by CARD_1:def 7;
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