theorem :: POSET_2:27

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
for f1, g1, f2, g2 being Function of X,Y st E1,E2 is_well_founded_with_minimal_set D & ( for x being Element of X holds
( ( x in D implies ( f1 . x = I1 . x & g1 . x = I2 . x ) ) & ( not x in D implies ( f1 . x = J1 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] & g1 . x = J2 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] ) ) ) ) & ( for x being Element of X holds
( ( x in D implies ( f2 . x = I1 . x & g2 . x = I2 . x ) ) & ( not x in D implies ( f2 . x = J1 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] & g2 . x = J2 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] ) ) ) ) holds
( f1 = f2 & g1 = g2 )