theorem Threcursive0301:
for
X,
Y being non
empty set for
D being
Subset of
X for
I1,
I2 being
Function of
X,
Y for
J1,
J2 being
Function of
[:X,Y,Y:],
Y for
E1,
E2 being
Function of
X,
X st
E1,
E2 is_well_founded_with_minimal_set D holds
ex
f,
g being
continuous Function of
(FlatPoset X),
(FlatPoset Y) st
for
x being
Element of
X holds
(
f . x in Y &
f . x = BaseFunc02 (
x,
(f . (E1 . x)),
(g . (E2 . x)),
I1,
J1,
D) &
g . x in Y &
g . x = BaseFunc02 (
x,
(f . (E1 . x)),
(g . (E2 . x)),
I2,
J2,
D) )