theorem Threcursive02: :: POSET_2:19

for X, Y being non empty set
for D being Subset of X
for I being Function of X,Y
for J being Function of [:X,Y:],Y
for E being Function of X,X ex f being set st
( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc01 (f,E,I,J,D) )