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 sequence of COMPLEX by A1, RELSET_1:4;
defpred S1[ Nat, Element of COMPLEX , set ] means $3 = $2 + (ss . ($1 + 1));
A2: for n being Nat
for x being Element of COMPLEX ex y being Element of COMPLEX st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of COMPLEX ex y being Element of COMPLEX st S1[n,x,y]
let x be Element of COMPLEX ; :: thesis: ex y being Element of COMPLEX st S1[n,x,y]
reconsider y = x + (ss . (n + 1)) as Element of COMPLEX by XCMPLX_0:def 2;
take y ; :: thesis: S1[n,x,y]
thus S1[n,x,y] ; :: thesis: verum
end;
consider f being sequence of COMPLEX such that
A3: f . 0 = ss . 0 and
A4: for n being Nat holds S1[n,f . n,f . (n + 1)] from RECDEF_1:sch 2(A2);
 take f ; :: thesis: ( f . 0 = s . 0 & ( for n being Nat holds f . (n + 1) = (f . n) + (s . (n + 1)) ) )
thus f . 0 = s . 0 by A3; :: thesis: for n being Nat holds f . (n + 1) = (f . n) + (s . (n + 1))
let n be Nat; :: thesis: f . (n + 1) = (f . n) + (s . (n + 1))
reconsider n = n as Element of NAT by ORDINAL1:def 12;
S1[n,f . n,f . (n + 1)] by A4;
hence f . (n + 1) = (f . n) + (s . (n + 1)) ; :: thesis: verum