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))

proof

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

end;

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