theorem Threcursive01:
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
W being
continuous Function of
(FlatConF (X,Y)),
(FlatConF (X,Y)) st
for
f being
Element of
ConFuncs (
(FlatPoset X),
(FlatPoset Y)) holds
W . f = RecFunc01 (
f,
E,
I,
J,
D)