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 ; :: thesis: 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; :: thesis: verum