theorem :: POSET_2:21

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 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 . (E . x))] ) )