set D = rng N;

defpred S_{1}[ set , set , set ] means for a, b being R_eal

for s being Element of NAT st s = $1 & a = $2 & b = $3 holds

b = a + (N . (s + 1));

reconsider A = N . 0 as R_eal ;

A1: for n being Nat

for x being Element of ExtREAL ex y being Element of ExtREAL st S_{1}[n,x,y]

A2: ( F . 0 = A & ( for n being Nat holds S_{1}[n,F . n,F . (n + 1)] ) )
from RECDEF_1:sch 2(A1);

take F ; :: thesis: ( F . 0 = N . 0 & ( for n being Nat

for y being R_eal st y = F . n holds

F . (n + 1) = y + (N . (n + 1)) ) )

thus F . 0 = N . 0 by A2; :: thesis: for n being Nat

for y being R_eal st y = F . n holds

F . (n + 1) = y + (N . (n + 1))

let n be Nat; :: thesis: for y being R_eal st y = F . n holds

F . (n + 1) = y + (N . (n + 1))

reconsider n = n as Element of NAT by ORDINAL1:def 12;

S_{1}[n,F . n,F . (n + 1)]
by A2;

hence for y being R_eal st y = F . n holds

F . (n + 1) = y + (N . (n + 1)) ; :: thesis: verum

defpred S

for s being Element of NAT st s = $1 & a = $2 & b = $3 holds

b = a + (N . (s + 1));

reconsider A = N . 0 as R_eal ;

A1: for n being Nat

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

proof

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

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

reconsider y = x + (N . (n + 1)) as R_eal ;

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

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

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

reconsider y = x + (N . (n + 1)) as R_eal ;

take y ; :: thesis: S

thus S

A2: ( F . 0 = A & ( for n being Nat holds S

take F ; :: thesis: ( F . 0 = N . 0 & ( for n being Nat

for y being R_eal st y = F . n holds

F . (n + 1) = y + (N . (n + 1)) ) )

thus F . 0 = N . 0 by A2; :: thesis: for n being Nat

for y being R_eal st y = F . n holds

F . (n + 1) = y + (N . (n + 1))

let n be Nat; :: thesis: for y being R_eal st y = F . n holds

F . (n + 1) = y + (N . (n + 1))

reconsider n = n as Element of NAT by ORDINAL1:def 12;

S

hence for y being R_eal st y = F . n holds

F . (n + 1) = y + (N . (n + 1)) ; :: thesis: verum