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 Element of NAT holds g . (n + 1),a = the addF of R . a,(g . n,a) ) ) from BINOM:sch 1();
take g ; :: thesis: for a being Element of R holds
( g . 0 ,a = 0. R & ( for n being Element of 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 Element of NAT holds g . (n + 1),a = a + (g . n,a) ) ) by A1; :: thesis: verum