reconsider X = X as non empty complex-membered set by a0;
reconsider s = s as sequence of X ;
defpred S₁[ Nat, Element of X, set ] means $3 = $2 + (s . ($1 + 1));
a1: for n being Element of NAT
for x being Element of X ex y being Element of X st S₁[n,x,y]

proof

let n be Element of NAT ; :: thesis: for x being Element of X ex y being Element of X st S₁[n,x,y]
let x be Element of X; :: thesis: ex y being Element of X st S₁[n,x,y]
reconsider y = x + (s . (n + 1)) as Element of X by a0, MEMBERED:def 25;
take y ; :: thesis: S₁[n,x,y]
thus S₁[n,x,y] ; :: thesis: verum

end;

ex f being Function of NAT,X st
( f . 0 = s . 0 & ( for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(a1);
hence ex b₁ being sequence of X st
( b₁ . 0 = s . 0 & ( for n being Element of NAT holds b₁ . (n + 1) = (b₁ . n) + (s . (n + 1)) ) ) ; :: thesis: verum