set D = rng N;
defpred S1[ 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 S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of ExtREAL ex y being Element of ExtREAL st S1[n,x,y]
let x be Element of ExtREAL ; :: thesis: ex y being Element of ExtREAL st S1[n,x,y]
reconsider y = x + (N . (n + 1)) as R_eal ;
take y ; :: thesis: S1[n,x,y]
thus S1[n,x,y] ; :: thesis: verum
end;
consider F being sequence of ExtREAL such that
A2: ( F . 0 = A & ( for n being Nat holds S1[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;
S1[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