theorem Threcursive0201:
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 ex
f,
g being
set st
(
f in ConFuncs (
(FlatPoset X),
(FlatPoset Y)) &
g in ConFuncs (
(FlatPoset X),
(FlatPoset Y)) &
f = RecFunc02 (
f,
g,
E1,
E2,
I1,
J1,
D) &
g = RecFunc02 (
f,
g,
E1,
E2,
I2,
J2,
D) )