defpred S1[ 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 S1[k,x]
consider p being FinSequence of REAL n such that
A2:
( dom p = Seg n & ( for k being Nat st k in Seg n holds
S1[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 b1 being FinSequence of REAL n st
( len b1 = n & ( for i being Nat st 1 <= i & i <= n holds
b1 . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) )
by A3, FINSEQ_1:6; verum