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 f . x = BaseFunc01 (x,(f . (E . x)),I,J,D)
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 f . x = BaseFunc01 (x,(f . (E . x)),I,J,D)
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 f . x = BaseFunc01 (x,(f . (E . x)),I,J,D)
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 f . x = BaseFunc01 (x,(f . (E . x)),I,J,D)
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 f . x = BaseFunc01 (x,(f . (E . x)),I,J,D) )
assume A1:
E is_well_founded_with_minimal_set D
; 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
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;
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;
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)
; verum