theorem Threcursive0101: :: POSET_2:23

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 ex W being continuous Function of [:(FlatConF (X,Y)),(FlatConF (X,Y)):],(FlatConF (X,Y)) st
for f being set st f in [:(ConFuncs ((FlatPoset X),(FlatPoset Y))),(ConFuncs ((FlatPoset X),(FlatPoset Y))):] holds
W . f = RecFunc02 ((f `1),(f `2),E1,E2,I,J,D)