defpred S1[ Nat, Real] means ex i being Element of NAT st
( $1 = i & $2 = integral ((proj (i,n)) * f) );
A1: for i being Nat st i in Seg n holds
ex x being Element of REAL st S1[i,x]
proof
let i be Nat; :: thesis: ( i in Seg n implies ex x being Element of REAL st S1[i,x] )
assume i in Seg n ; :: thesis: ex x being Element of REAL st S1[i,x]
then reconsider ii = i as Element of NAT ;
reconsider x = integral ((proj (ii,n)) * f) as Element of REAL by XREAL_0:def 1;
take x ; :: thesis: S1[i,x]
thus S1[i,x] ; :: thesis: verum
end;
consider p being FinSequence of REAL such that
A2: ( dom p = Seg n & ( for i being Nat st i in Seg n holds
S1[i,p . i] ) ) from FINSEQ_1:sch 5(A1);
 take p ; :: thesis: ( p is Element of REAL n & dom p = Seg n & ( for i being Element of NAT st i in Seg n holds
p . i = integral ((proj (i,n)) * f) ) )
A3: for i being Element of NAT st i in Seg n holds
p . i = integral ((proj (i,n)) * f)
proof
let i be Element of NAT ; :: thesis: ( i in Seg n implies p . i = integral ((proj (i,n)) * f) )
assume i in Seg n ; :: thesis: p . i = integral ((proj (i,n)) * f)
then S1[i,p . i] by A2;
hence p . i = integral ((proj (i,n)) * f) ; :: thesis: verum
end;
len p = n by A2, FINSEQ_1:def 3;
hence ( p is Element of REAL n & dom p = Seg n & ( for i being Element of NAT st i in Seg n holds
p . i = integral ((proj (i,n)) * f) ) ) by A2, A3, FINSEQ_2:92; :: thesis: verum