let X, Y be 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))] ) )
let D be 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 I be 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 J be 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 E be Function of X,X; ( 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
; 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
; 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; ( ( 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; verum