let X, Y be non empty set ; :: thesis: 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))] ) )
let D be Subset of X; :: thesis: 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))] ) )
let I be Function of X,Y; :: thesis: 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))] ) )
let J be Function of [:X,Y,Y:],Y; :: thesis: 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))] ) )
let E1, E2 be Function of X,X; :: thesis: ( E1,E2 is_well_founded_with_minimal_set D implies 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))] ) ) )
assume E1,E2 is_well_founded_with_minimal_set D ; :: thesis: 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))] ) )
then consider f, g being Function of X,Y such that
A1: for x being Element of X holds
( ( x in D implies ( f . x = I . x & g . x = I . x ) ) & ( not x in D implies ( f . x = J . [x,(f . (E1 . x)),(g . (E2 . x))] & g . x = J . [x,(f . (E1 . x)),(g . (E2 . x))] ) ) ) by Threcursive05;
for x being Element of X holds f . x = g . x

proof

let x be Element of X; :: thesis: f . x = g . x

per cases ( x in D or not x in D ) ;

suppose C0: x in D ; :: thesis: f . x = g . x

then f . x = I . x by A1
.= g . x by A1, C0 ;
hence f . x = g . x ; :: thesis: verum

end;

suppose C0: not x in D ; :: thesis: f . x = g . x

then f . x = J . [x,(f . (E1 . x)),(g . (E2 . x))] by A1
.= g . x by A1, C0 ;
hence f . x = g . x ; :: thesis: verum

end;

end;

end;

then f = g ;
then 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))] ) ) by A1;
hence 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))] ) ) ; :: thesis: verum