set X = COMPLEX ;
A1: dom s = NAT by PARTFUN1:def 2;
rng s c= COMPLEX by VALUED_0:def 1;
then reconsider ss = s as Function of NAT,COMPLEX by A1, RELSET_1:4;
defpred S₁[ Nat, Element of COMPLEX , set ] means $3 = $2 + (ss . ($1 + 1));
A2: for n being Element of NAT
for x being Element of COMPLEX ex y being Element of COMPLEX st S₁[n,x,y] ;
ex f being Function of NAT,COMPLEX st
( f . 0 = ss . 0 & ( for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A2);
hence ex b₁ being complex-valued ManySortedSet of NAT st
( b₁ . 0 = s . 0 & ( for n being Element of NAT holds b₁ . (n + 1) = (b₁ . n) + (s . (n + 1)) ) ) ; :: thesis: verum