theorem Threcursive03:
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 st
E is_well_founded_with_minimal_set D holds
ex
f being
continuous Function of
(FlatPoset X),
(FlatPoset Y) st
for
x being
Element of
X holds
(
f . x in Y &
f . x = BaseFunc01 (
x,
(f . (E . x)),
I,
J,
D) )