theorem
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 st
E1,
E2 is_well_founded_with_minimal_set D holds
ex
f being
Function of
X,
Y st
for
x being
Element of
X holds
( (
x in D implies
f . x = I . x ) & ( not
x in D implies
f . x = J . [x,(f . (E1 . x)),(f . (E2 . x))] ) )