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 f . x = BaseFunc01 (x,(f . (E . x)),I,J,D)
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 f . x = BaseFunc01 (x,(f . (E . x)),I,J,D)
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 f . x = BaseFunc01 (x,(f . (E . x)),I,J,D)
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 f . x = BaseFunc01 (x,(f . (E . x)),I,J,D)
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 f . x = BaseFunc01 (x,(f . (E . x)),I,J,D) )
assume A1: E is_well_founded_with_minimal_set D ; :: thesis: ex f being Function of X,Y st
for x being Element of X holds f . x = BaseFunc01 (x,(f . (E . x)),I,J,D)
set FX = FlatPoset X;
set CX = succ X;
A02: X c= succ X by XBOOLE_1:7;
set FY = FlatPoset Y;
set CY = succ Y;
consider f1 being continuous Function of (FlatPoset X),(FlatPoset Y) such that
A3: for x being Element of X holds
( f1 . x in Y & f1 . x = BaseFunc01 (x,(f1 . (E . x)),I,J,D) ) by A1, Threcursive03;
reconsider f1 = f1 as Function of (succ X),(succ Y) ;
reconsider f = f1 | X as Function of X,(succ Y) by A02, FUNCT_2:32;
for x being Element of X holds f . x in Y

proof

let x be Element of X; :: thesis: f . x in Y
f1 . x in Y by A3;
hence f . x in Y by FUNCT_1:49; :: thesis: verum

end;

then rng f c= Y by FUNCT_2:114;
then reconsider f = f as Function of X,Y by FUNCT_2:6;
for x being Element of X holds f . x = BaseFunc01 (x,(f . (E . x)),I,J,D)

proof

let x be Element of X; :: thesis: f . x = BaseFunc01 (x,(f . (E . x)),I,J,D)
reconsider x1 = E . x as Element of X ;
f . x = f1 . x by FUNCT_1:49
.= BaseFunc01 (x,(f1 . x1),I,J,D) by A3 ;
hence f . x = BaseFunc01 (x,(f . (E . x)),I,J,D) by FUNCT_1:49; :: thesis: verum

end;

hence ex f being Function of X,Y st
for x being Element of X holds f . x = BaseFunc01 (x,(f . (E . x)),I,J,D) ; :: thesis: verum