:: deftheorem DefRecFunc02 defines RecFunc02 POSET_2:def 12 :
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:],Y
for E1, E2 being Function of X,X
for h1, h2 being object st h1 is continuous Function of (FlatPoset X),(FlatPoset Y) & h2 is continuous Function of (FlatPoset X),(FlatPoset Y) holds
for b10 being continuous Function of (FlatPoset X),(FlatPoset Y) holds
( b10 = RecFunc02 (h1,h2,E1,E2,I,J,D) iff for x being Element of (FlatPoset X)
for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds
b10 . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D) );