defpred S_{1}[ Nat, Real] means ex i being Element of NAT ex Fi being FinSequence of REAL st

( $1 = i & Fi = (proj (i,n)) * F & $2 = Sum Fi );

A1: for i being Nat st i in Seg n holds

ex x being Element of REAL st S_{1}[i,x]

A2: ( dom p = Seg n & ( for i being Nat st i in Seg n holds

S_{1}[i,p . i] ) )
from FINSEQ_1:sch 5(A1);

take p ; :: thesis: ( p is Element of REAL n & ( for i being Element of NAT st i in Seg n holds

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & p . i = Sum Fi ) ) )

A3: for i being Element of NAT st i in Seg n holds

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & p . i = Sum Fi )

hence ( p is Element of REAL n & ( for i being Element of NAT st i in Seg n holds

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & p . i = Sum Fi ) ) ) by A3, FINSEQ_2:92; :: thesis: verum

( $1 = i & Fi = (proj (i,n)) * F & $2 = Sum Fi );

A1: for i being Nat st i in Seg n holds

ex x being Element of REAL st S

proof

consider p being FinSequence of REAL such that
let i be Nat; :: thesis: ( i in Seg n implies ex x being Element of REAL st S_{1}[i,x] )

assume i in Seg n ; :: thesis: ex x being Element of REAL st S_{1}[i,x]

then reconsider ii = i as Element of NAT ;

reconsider Fi = (proj (ii,n)) * F as FinSequence of REAL ;

reconsider x = Sum Fi as Element of REAL by XREAL_0:def 1;

take x ; :: thesis: S_{1}[i,x]

thus ex ii being Element of NAT ex Fi being FinSequence of REAL st

( i = ii & Fi = (proj (ii,n)) * F & x = Sum Fi ) ; :: thesis: verum

end;assume i in Seg n ; :: thesis: ex x being Element of REAL st S

then reconsider ii = i as Element of NAT ;

reconsider Fi = (proj (ii,n)) * F as FinSequence of REAL ;

reconsider x = Sum Fi as Element of REAL by XREAL_0:def 1;

take x ; :: thesis: S

thus ex ii being Element of NAT ex Fi being FinSequence of REAL st

( i = ii & Fi = (proj (ii,n)) * F & x = Sum Fi ) ; :: thesis: verum

A2: ( dom p = Seg n & ( for i being Nat st i in Seg n holds

S

take p ; :: thesis: ( p is Element of REAL n & ( for i being Element of NAT st i in Seg n holds

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & p . i = Sum Fi ) ) )

A3: for i being Element of NAT st i in Seg n holds

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & p . i = Sum Fi )

proof

len p = n
by A2, FINSEQ_1:def 3;
let i be Element of NAT ; :: thesis: ( i in Seg n implies ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & p . i = Sum Fi ) )

reconsider k = i as Nat ;

assume i in Seg n ; :: thesis: ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & p . i = Sum Fi )

then S_{1}[k,p . k]
by A2;

hence ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & p . i = Sum Fi ) ; :: thesis: verum

end;( Fi = (proj (i,n)) * F & p . i = Sum Fi ) )

reconsider k = i as Nat ;

assume i in Seg n ; :: thesis: ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & p . i = Sum Fi )

then S

hence ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & p . i = Sum Fi ) ; :: thesis: verum

hence ( p is Element of REAL n & ( for i being Element of NAT st i in Seg n holds

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & p . i = Sum Fi ) ) ) by A3, FINSEQ_2:92; :: thesis: verum