defpred S₁[ Nat, Element of 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 );
PN: for i being Nat st i in Seg n holds
ex x being Element of REAL st S₁[i,x]

proof

let i be Nat; :: thesis: ( i in Seg n implies ex x being Element of REAL st S₁[i,x] )
assume i in Seg n ; :: thesis: ex x being Element of REAL st S₁[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 ;
take x ; :: thesis: S₁[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;

consider p being FinSequence of REAL such that
A1: ( dom p = Seg n & ( for i being Nat st i in Seg n holds
S₁[i,p . i] ) ) from FINSEQ_1:sch 5(PN);
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 ) ) )
A2: len p = n by A1, FINSEQ_1:def 3;
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

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 ) )
assume F0: i in Seg n ; :: thesis: ex Fi being FinSequence of REAL st
( Fi = (proj i,n) * F & p . i = Sum Fi )
reconsider k = i as Nat ;
S₁[k,p . k] by A1, F0;
hence ex Fi being FinSequence of REAL st
( Fi = (proj i,n) * F & p . i = Sum Fi ) ; :: thesis: verum

end;

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 A2, FINSEQ_2:110; :: thesis: verum