set D = the carrier of R;
consider g being Function of [:NAT, the carrier of R:], the carrier of R such that
A1:
for a being Element of the carrier of R holds
( g . (0,a) = 0. R & ( for n being Nat holds g . ((n + 1),a) = the addF of R . (a,(g . (n,a))) ) )
by Lm1;
take
g
; for a being Element of R holds
( g . (0,a) = 0. R & ( for n being Nat holds g . ((n + 1),a) = a + (g . (n,a)) ) )
thus
for a being Element of R holds
( g . (0,a) = 0. R & ( for n being Nat holds g . ((n + 1),a) = a + (g . (n,a)) ) )
by A1; verum