:: deftheorem DefRecFunc01 defines RecFunc01 POSET_2:def 9 :
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
for h being object st h is continuous Function of (FlatPoset X),(FlatPoset Y) holds
for b₈ being continuous Function of (FlatPoset X),(FlatPoset Y) holds
( b₈ = RecFunc01 (h,E,I,J,D) iff for x being Element of (FlatPoset X)
for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds
b₈ . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) );