defpred S1[ 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 S1[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (len p) implies ex x being Element of REAL st S1[k,x] )
assume k in Seg (len p) ; :: thesis: ex x being Element of REAL st S1[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 S1[k,x]
reconsider ll = log (a,(p . k)) as Element of REAL by XREAL_0:def 1;
take ll ; :: thesis: S1[k,ll]
thus S1[k,ll] by A4; :: thesis: verum
end;
suppose A5: p . k = 0 ; :: thesis: ex x being Element of REAL st S1[k,x]
take In (0,REAL) ; :: thesis: S1[k, In (0,REAL)]
thus S1[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
S1[k,pp . k] ) ) from FINSEQ_1:sch 5(A2);
 len pp = len p by A6, FINSEQ_1:def 3;
hence ex b1 being FinSequence of REAL st
( len b1 = len p & ( for k being Nat st k in dom b1 holds
( ( p . k > 0 implies b1 . k = log (a,(p . k)) ) & ( p . k = 0 implies b1 . k = 0 ) ) ) ) by A6; :: thesis: verum