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
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))] ) )
let D be Subset of X; :: thesis: 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))] ) )
let I be Function of X,Y; :: thesis: 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))] ) )
let J be Function of [:X,Y:],Y; :: thesis: 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))] ) )
let E be Function of X,X; :: thesis: ( E 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 . (E . x))] ) ) )
assume E 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 . (E . x))] ) )
then consider f being Function of X,Y such that
A1: for x being Element of X holds f . x = BaseFunc01 (x,(f . (E . x)),I,J,D) by Lemrecursive04;
take f ; :: thesis: 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))] ) )
let x be Element of X; :: thesis: ( ( x in D implies f . x = I . x ) & ( not x in D implies f . x = J . [x,(f . (E . x))] ) )
f . x = BaseFunc01 (x,(f . (E . x)),I,J,D) by A1;
hence ( ( x in D implies f . x = I . x ) & ( not x in D implies f . x = J . [x,(f . (E . x))] ) ) by DefBaseFunc01; :: thesis: verum