defpred S₁[ set , set ] means for i being Nat st i = $1 & 1 <= i & i <= n holds
$2 = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i));
A1: for k being Nat st k in Seg n holds
ex x being Element of REAL n st S₁[k,x]

proof

reconsider n0 = n as Element of NAT by ORDINAL1:def 12;
let k be Nat; :: thesis: ( k in Seg n implies ex x being Element of REAL n st S₁[k,x] )
assume k in Seg n ; :: thesis: ex x being Element of REAL n st S₁[k,x]
reconsider k0 = k as Element of NAT by ORDINAL1:def 12;
reconsider x00 = |(x0,(Base_FinSeq (n0,k0)))| * (Base_FinSeq (n0,k0)) as Element of REAL n ;
for i being Nat st i = k & 1 <= i & i <= n holds
x00 = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ;
hence ex x being Element of REAL n st S₁[k,x] ; :: thesis: verum

end;

consider p being FinSequence of REAL n such that
A2: ( dom p = Seg n & ( for k being Nat st k in Seg n holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 5(A1);
A3: for i being Nat st 1 <= i & i <= n holds
p . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) by FINSEQ_1:1, A2;
Seg n = Seg (len p) by A2, FINSEQ_1:def 3;
hence ex b₁ being FinSequence of REAL n st
( len b₁ = n & ( for i being Nat st 1 <= i & i <= n holds
b₁ . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) ) by A3, FINSEQ_1:6; :: thesis: verum