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 continuous Function of (FlatPoset X),(FlatPoset Y) st
for x being Element of X holds
( f . x in Y & 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 continuous Function of (FlatPoset X),(FlatPoset Y) st
for x being Element of X holds
( f . x in Y & 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 continuous Function of (FlatPoset X),(FlatPoset Y) st
for x being Element of X holds
( f . x in Y & 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 continuous Function of (FlatPoset X),(FlatPoset Y) st
for x being Element of X holds
( f . x in Y & 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 continuous Function of (FlatPoset X),(FlatPoset Y) st
for x being Element of X holds
( f . x in Y & f . x = BaseFunc01 (x,(f . (E . x)),I,J,D) ) )
set z = X;
set r = Y;
assume A0: E is_well_founded_with_minimal_set D ; :: thesis: ex f being continuous Function of (FlatPoset X),(FlatPoset Y) st
for x being Element of X holds
( f . x in Y & f . x = BaseFunc01 (x,(f . (E . x)),I,J,D) )
A1: ( not X in X & not Y in Y ) ;
set FX = FlatPoset X;
set CX = succ X;
set FY = FlatPoset Y;
set CY = succ Y;
consider f being set such that
A5: ( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc01 (f,E,I,J,D) ) by Threcursive02;
reconsider f = f as continuous Function of (FlatPoset X),(FlatPoset Y) by A5;
consider l being Function of X,NAT such that
A6: for x0 being Element of X holds
( ( l . x0 <= 0 implies x0 in D ) & ( not x0 in D implies l . (E . x0) < l . x0 ) ) by A0;
defpred S₁[ Nat] means for x0 being Element of X st l . x0 <= $1 holds
( f . x0 in Y & f . x0 = BaseFunc01 (x0,(f . (E . x0)),I,J,D) );
A7: S₁[ 0 ]

proof

let x0 be Element of X; :: thesis: ( l . x0 <= 0 implies ( f . x0 in Y & f . x0 = BaseFunc01 (x0,(f . (E . x0)),I,J,D) ) )
assume b1: l . x0 <= 0 ; :: thesis: ( f . x0 in Y & f . x0 = BaseFunc01 (x0,(f . (E . x0)),I,J,D) )
B2: x0 in X ;
reconsider x0 = x0 as Element of (FlatPoset X) by XBOOLE_0:def 3;
B3: x0 <> X by B2;
B5: f . x0 = BaseFunc01 (x0,(f . ((Flatten E) . x0)),I,J,D) by DefRecFunc01, A5
.= BaseFunc01 (x0,(f . (E . x0)),I,J,D) by B3, DefFlatten04 ;
then f . x0 = I . x0 by DefBaseFunc01, b1, A6;
hence ( f . x0 in Y & f . x0 = BaseFunc01 (x0,(f . (E . x0)),I,J,D) ) by B5, FUNCT_2:5; :: thesis: verum

end;

A8: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B0: S₁[k] ; :: thesis: S₁[k + 1]
let x0 be Element of X; :: thesis: ( l . x0 <= k + 1 implies ( f . x0 in Y & f . x0 = BaseFunc01 (x0,(f . (E . x0)),I,J,D) ) )
assume B1: l . x0 <= k + 1 ; :: thesis: ( f . x0 in Y & f . x0 = BaseFunc01 (x0,(f . (E . x0)),I,J,D) )
reconsider x0 = x0 as Element of (FlatPoset X) by XBOOLE_0:def 3;
B3: x0 <> X by A1;
reconsider x1 = E . x0 as Element of X by FUNCT_2:5;
B5: f . x0 = BaseFunc01 (x0,(f . ((Flatten E) . x0)),I,J,D) by DefRecFunc01, A5
.= BaseFunc01 (x0,(f . x1),I,J,D) by B3, DefFlatten04 ;

per cases ( x0 in D or not x0 in D ) ;

suppose x0 in D ; :: thesis: ( f . x0 in Y & f . x0 = BaseFunc01 (x0,(f . (E . x0)),I,J,D) )

then f . x0 = I . x0 by DefBaseFunc01, B5;
hence ( f . x0 in Y & f . x0 = BaseFunc01 (x0,(f . (E . x0)),I,J,D) ) by FUNCT_2:5, B5; :: thesis: verum

end;

suppose C0: not x0 in D ; :: thesis: ( f . x0 in Y & f . x0 = BaseFunc01 (x0,(f . (E . x0)),I,J,D) )

reconsider x0 = x0 as Element of X ;
(l . x1) + 1 <= l . x0 by NAT_1:13, A6, C0;
then (l . x1) + 1 <= k + 1 by B1, XXREAL_0:2;
then l . x1 <= k by XREAL_1:8;
then C1: f . x1 in Y by B0;
C4: [x0,(f . x1)] in [:X,Y:] by C1, ZFMISC_1:def 2;
J . [x0,(f . x1)] in Y by C4, FUNCT_2:5;
hence ( f . x0 in Y & f . x0 = BaseFunc01 (x0,(f . (E . x0)),I,J,D) ) by B5, DefBaseFunc01, C0, C1; :: thesis: verum

end;

end;

end;

A9: for k being Nat holds S₁[k] from NAT_1:sch 2(A7, A8);
for x being Element of X holds
( f . x in Y & f . x = BaseFunc01 (x,(f . (E . x)),I,J,D) )

proof

let x be Element of X; :: thesis: ( f . x in Y & f . x = BaseFunc01 (x,(f . (E . x)),I,J,D) )
reconsider k = l . x as Nat ;
l . x <= k ;
hence ( f . x in Y & f . x = BaseFunc01 (x,(f . (E . x)),I,J,D) ) by A9; :: thesis: verum

end;

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