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 S_{1}[ 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 S_{1}[n,x,y]

A3: f . 0 = ss . 0 and

A4: for n being Nat holds S_{1}[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;

S_{1}[n,f . n,f . (n + 1)]
by A4;

hence f . (n + 1) = (f . n) + (s . (n + 1)) ; :: thesis: verum

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 S

A2: for n being Nat

for x being Element of COMPLEX ex y being Element of COMPLEX st S

proof

consider f being sequence of COMPLEX such that
let n be Nat; :: thesis: for x being Element of COMPLEX ex y being Element of COMPLEX st S_{1}[n,x,y]

let x be Element of COMPLEX ; :: thesis: ex y being Element of COMPLEX st S_{1}[n,x,y]

reconsider y = x + (ss . (n + 1)) as Element of COMPLEX by XCMPLX_0:def 2;

take y ; :: thesis: S_{1}[n,x,y]

thus S_{1}[n,x,y]
; :: thesis: verum

end;let x be Element of COMPLEX ; :: thesis: ex y being Element of COMPLEX st S

reconsider y = x + (ss . (n + 1)) as Element of COMPLEX by XCMPLX_0:def 2;

take y ; :: thesis: S

thus S

A3: f . 0 = ss . 0 and

A4: for n being Nat holds S

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;

S

hence f . (n + 1) = (f . n) + (s . (n + 1)) ; :: thesis: verum