theorem :: BINOM:26

for C, D being non empty set
for b being Element of D
for F being Function of [:C,D:],D ex g being Function of [:NAT,C:],D st
for a being Element of C holds
( g . (0,a) = b & ( for n being Nat holds g . ((n + 1),a) = F . (a,(g . (n,a))) ) ) by Lm1;