let X, Y be 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 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; 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; 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; 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; ( 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
; 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
; 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
; 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; ( ( 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; verum