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 ) ) from BINOM:sch 2();
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