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