defpred S₁[ Nat, Element of R] means $2 = (p /. $1) + (q /. $1);
A1: for k being Nat st k in Seg (len p) holds
ex x being Element of R st S₁[k,x] ;
consider f being FinSequence of the carrier of R such that
A2: ( dom f = Seg (len p) & ( for k being Nat st k in Seg (len p) holds
S₁[k,f /. k] ) ) from RECDEF_1:sch 17(A1);
take f ; :: thesis: ( dom f = dom p & ( for i being Nat st 1 <= i & i <= len f holds
f /. i = (p /. i) + (q /. i) ) )
A3: len f = len p by A2, FINSEQ_1:def 3;
for m being Nat st 1 <= m & m <= len f holds
f /. m = (p /. m) + (q /. m) by A2, A3, FINSEQ_1:1;
hence ( dom f = dom p & ( for i being Nat st 1 <= i & i <= len f holds
f /. i = (p /. i) + (q /. i) ) ) by A2, FINSEQ_1:def 3; :: thesis: verum