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 ex f being set st
( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc01 (f,E,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 ex f being set st
( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc01 (f,E,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 ex f being set st
( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc01 (f,E,I,J,D) )
let J be Function of [:X,Y:],Y; :: thesis: for E being Function of X,X ex f being set st
( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc01 (f,E,I,J,D) )
let E be Function of X,X; :: thesis: ex f being set st
( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc01 (f,E,I,J,D) )
set FX = FlatPoset X;
set FY = FlatPoset Y;
set FlatC = FlatConF (X,Y);
set CFXY = ConFuncs ((FlatPoset X),(FlatPoset Y));
set CRFXY = ConRelat ((FlatPoset X),(FlatPoset Y));
consider W being continuous Function of (FlatConF (X,Y)),(FlatConF (X,Y)) such that
A4: for f being Element of ConFuncs ((FlatPoset X),(FlatPoset Y)) holds W . f = RecFunc01 (f,E,I,J,D) by Threcursive01;
reconsider W = W as monotone Function of (FlatConF (X,Y)),(FlatConF (X,Y)) ;
reconsider f = least_fix_point W as Element of (FlatConF (X,Y)) ;
A5: f is_a_fixpoint_of W by POSET_1:def 5;
A6: f = W . f by A5, ABIAN:def 3;
take f ; :: thesis: ( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc01 (f,E,I,J,D) )
thus ( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc01 (f,E,I,J,D) ) by A4, A6; :: thesis: verum