defpred S₁[ Nat, set ] means ( ( p . $1 > 0 implies $2 = log (a,(p . $1)) ) & ( p . $1 = 0 implies $2 = 0 ) );
A2: for k being Nat st k in Seg (len p) holds
ex x being Element of REAL st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len p) implies ex x being Element of REAL st S₁[k,x] )
assume k in Seg (len p) ; :: thesis: ex x being Element of REAL st S₁[k,x]
then A3: k in dom p by FINSEQ_1:def 3;

per cases ( p . k > 0 or p . k = 0 ) by A1, A3;

suppose A4: p . k > 0 ; :: thesis: ex x being Element of REAL st S₁[k,x]

reconsider ll = log (a,(p . k)) as Element of REAL by XREAL_0:def 1;
take ll ; :: thesis: S₁[k,ll]
thus S₁[k,ll] by A4; :: thesis: verum

end;

suppose A5: p . k = 0 ; :: thesis: ex x being Element of REAL st S₁[k,x]

take In (0,REAL) ; :: thesis: S₁[k, In (0,REAL)]
thus S₁[k, In (0,REAL)] by A5; :: thesis: verum

end;

end;

end;

consider pp being FinSequence of REAL such that
A6: ( dom pp = Seg (len p) & ( for k being Nat st k in Seg (len p) holds
S₁[k,pp . k] ) ) from FINSEQ_1:sch 5(A2);
len pp = len p by A6, FINSEQ_1:def 3;
hence ex b₁ being FinSequence of REAL st
( len b₁ = len p & ( for k being Nat st k in dom b₁ holds
( ( p . k > 0 implies b₁ . k = log (a,(p . k)) ) & ( p . k = 0 implies b₁ . k = 0 ) ) ) ) by A6; :: thesis: verum