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

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 n0 = n as Element of NAT by ORDINAL1:def 13;
reconsider k0 = k as Element of NAT by ORDINAL1:def 13;
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: Seg n = Seg (len p) by A2, FINSEQ_1:def 3;
for i being Nat st 1 <= i & i <= n holds
p . i = |(x0,(Base_FinSeq n,i))| * (Base_FinSeq n,i)

proof

let i be Nat; :: thesis: ( 1 <= i & i <= n implies p . i = |(x0,(Base_FinSeq n,i))| * (Base_FinSeq n,i) )
assume A4: ( 1 <= i & i <= n ) ; :: thesis: p . i = |(x0,(Base_FinSeq n,i))| * (Base_FinSeq n,i)
then i in Seg n by FINSEQ_1:3;
hence p . i = |(x0,(Base_FinSeq n,i))| * (Base_FinSeq n,i) by A2, A4; :: thesis: verum

end;

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:8; :: thesis: verum