let D be Denum_Set_of_R_EAL; :: thesis: for N being Num of D ex F being Function of NAT,ExtREAL st
( F . 0 = N . 0 & ( for n being Element of NAT
for y being R_eal st y = F . n holds
F . (n + 1) = y + (N . (n + 1)) ) )
let N be Num of D; :: thesis: ex F being Function of NAT,ExtREAL st
( F . 0 = N . 0 & ( for n being Element of NAT
for y being R_eal st y = F . n holds
F . (n + 1) = y + (N . (n + 1)) ) )
defpred S₁[ 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 Element of NAT
for x being Element of ExtREAL ex y being Element of ExtREAL st S₁[n,x,y]

proof

let n be Element of NAT ; :: thesis: for x being Element of ExtREAL ex y being Element of ExtREAL st S₁[n,x,y]
let x be Element of ExtREAL ; :: thesis: ex y being Element of ExtREAL st S₁[n,x,y]
reconsider y = x + (N . (n + 1)) as R_eal ;
take y ; :: thesis: S₁[n,x,y]
thus S₁[n,x,y] ; :: thesis: verum

end;

consider F being Function of NAT,ExtREAL such that
A2: ( F . 0 = A & ( for n being Element of NAT holds S₁[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A1);
take F ; :: thesis: ( F . 0 = N . 0 & ( for n being Element of NAT
for y being R_eal st y = F . n holds
F . (n + 1) = y + (N . (n + 1)) ) )
thus ( F . 0 = N . 0 & ( for n being Element of NAT
for y being R_eal st y = F . n holds
F . (n + 1) = y + (N . (n + 1)) ) ) by A2; :: thesis: verum