let X, Y be non empty set ; :: thesis: 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 st E1,E2 is_well_founded_with_minimal_set D holds
ex f, g being Function of X,Y st
for x being Element of X holds
( ( x in D implies ( f . x = I1 . x & g . x = I2 . x ) ) & ( not x in D implies ( f . x = J1 . [x,(f . (E1 . x)),(g . (E2 . x))] & g . x = J2 . [x,(f . (E1 . x)),(g . (E2 . x))] ) ) )
let D be Subset of X; :: thesis: 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 st E1,E2 is_well_founded_with_minimal_set D holds
ex f, g being Function of X,Y st
for x being Element of X holds
( ( x in D implies ( f . x = I1 . x & g . x = I2 . x ) ) & ( not x in D implies ( f . x = J1 . [x,(f . (E1 . x)),(g . (E2 . x))] & g . x = J2 . [x,(f . (E1 . x)),(g . (E2 . x))] ) ) )
let I1, I2 be Function of X,Y; :: thesis: for J1, J2 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, g being Function of X,Y st
for x being Element of X holds
( ( x in D implies ( f . x = I1 . x & g . x = I2 . x ) ) & ( not x in D implies ( f . x = J1 . [x,(f . (E1 . x)),(g . (E2 . x))] & g . x = J2 . [x,(f . (E1 . x)),(g . (E2 . x))] ) ) )
let J1, J2 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, g being Function of X,Y st
for x being Element of X holds
( ( x in D implies ( f . x = I1 . x & g . x = I2 . x ) ) & ( not x in D implies ( f . x = J1 . [x,(f . (E1 . x)),(g . (E2 . x))] & g . x = J2 . [x,(f . (E1 . x)),(g . (E2 . x))] ) ) )
let E1, E2 be Function of X,X; :: thesis: ( E1,E2 is_well_founded_with_minimal_set D implies ex f, g being Function of X,Y st
for x being Element of X holds
( ( x in D implies ( f . x = I1 . x & g . x = I2 . x ) ) & ( not x in D implies ( f . x = J1 . [x,(f . (E1 . x)),(g . (E2 . x))] & g . x = J2 . [x,(f . (E1 . x)),(g . (E2 . x))] ) ) ) )
assume E1,E2 is_well_founded_with_minimal_set D ; :: thesis: ex f, g being Function of X,Y st
for x being Element of X holds
( ( x in D implies ( f . x = I1 . x & g . x = I2 . x ) ) & ( not x in D implies ( f . x = J1 . [x,(f . (E1 . x)),(g . (E2 . x))] & g . x = J2 . [x,(f . (E1 . x)),(g . (E2 . x))] ) ) )
then consider f, g being Function of X,Y such that
A1: for x being Element of X holds
( f . x = BaseFunc02 (x,(f . (E1 . x)),(g . (E2 . x)),I1,J1,D) & g . x = BaseFunc02 (x,(f . (E1 . x)),(g . (E2 . x)),I2,J2,D) ) by Lemrecursive0401;
take f ; :: thesis: ex g being Function of X,Y st
for x being Element of X holds
( ( x in D implies ( f . x = I1 . x & g . x = I2 . x ) ) & ( not x in D implies ( f . x = J1 . [x,(f . (E1 . x)),(g . (E2 . x))] & g . x = J2 . [x,(f . (E1 . x)),(g . (E2 . x))] ) ) )
take g ; :: thesis: for x being Element of X holds
( ( x in D implies ( f . x = I1 . x & g . x = I2 . x ) ) & ( not x in D implies ( f . x = J1 . [x,(f . (E1 . x)),(g . (E2 . x))] & g . x = J2 . [x,(f . (E1 . x)),(g . (E2 . x))] ) ) )
let x be Element of X; :: thesis: ( ( x in D implies ( f . x = I1 . x & g . x = I2 . x ) ) & ( not x in D implies ( f . x = J1 . [x,(f . (E1 . x)),(g . (E2 . x))] & g . x = J2 . [x,(f . (E1 . x)),(g . (E2 . x))] ) ) )
( f . x = BaseFunc02 (x,(f . (E1 . x)),(g . (E2 . x)),I1,J1,D) & g . x = BaseFunc02 (x,(f . (E1 . x)),(g . (E2 . x)),I2,J2,D) ) by A1;
hence ( ( x in D implies ( f . x = I1 . x & g . x = I2 . x ) ) & ( not x in D implies ( f . x = J1 . [x,(f . (E1 . x)),(g . (E2 . x))] & g . x = J2 . [x,(f . (E1 . x)),(g . (E2 . x))] ) ) ) by DefBaseFunc02; :: thesis: verum