let X, Y be non empty set ; :: thesis: 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 ex f, g being set st
( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & g in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc02 (f,g,E1,E2,I1,J1,D) & g = RecFunc02 (f,g,E1,E2,I2,J2,D) )
let D be Subset of X; :: thesis: 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 ex f, g being set st
( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & g in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc02 (f,g,E1,E2,I1,J1,D) & g = RecFunc02 (f,g,E1,E2,I2,J2,D) )
let I1, I2 be Function of X,Y; :: thesis: for J1, J2 being Function of [:X,Y,Y:],Y
for E1, E2 being Function of X,X ex f, g being set st
( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & g in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc02 (f,g,E1,E2,I1,J1,D) & g = RecFunc02 (f,g,E1,E2,I2,J2,D) )
let J1, J2 be Function of [:X,Y,Y:],Y; :: thesis: for E1, E2 being Function of X,X ex f, g being set st
( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & g in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc02 (f,g,E1,E2,I1,J1,D) & g = RecFunc02 (f,g,E1,E2,I2,J2,D) )
let E1, E2 be Function of X,X; :: thesis: ex f, g being set st
( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & g in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc02 (f,g,E1,E2,I1,J1,D) & g = RecFunc02 (f,g,E1,E2,I2,J2,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));
set FlatC2 = [:(FlatConF (X,Y)),(FlatConF (X,Y)):];
set CFXY2 = [:(ConFuncs ((FlatPoset X),(FlatPoset Y))),(ConFuncs ((FlatPoset X),(FlatPoset Y))):];
set CRFXY2 = ["(ConRelat ((FlatPoset X),(FlatPoset Y))),(ConRelat ((FlatPoset X),(FlatPoset Y)))"];
A4: ( the carrier of [:(FlatConF (X,Y)),(FlatConF (X,Y)):] = [:(ConFuncs ((FlatPoset X),(FlatPoset Y))),(ConFuncs ((FlatPoset X),(FlatPoset Y))):] & the InternalRel of [:(FlatConF (X,Y)),(FlatConF (X,Y)):] = ["(ConRelat ((FlatPoset X),(FlatPoset Y))),(ConRelat ((FlatPoset X),(FlatPoset Y)))"] ) by YELLOW_3:def 2;
consider W1 being continuous Function of [:(FlatConF (X,Y)),(FlatConF (X,Y)):],(FlatConF (X,Y)) such that
A5: for h being set st h in [:(ConFuncs ((FlatPoset X),(FlatPoset Y))),(ConFuncs ((FlatPoset X),(FlatPoset Y))):] holds
W1 . h = RecFunc02 ((h `1),(h `2),E1,E2,I1,J1,D) by Threcursive0101;
consider W2 being continuous Function of [:(FlatConF (X,Y)),(FlatConF (X,Y)):],(FlatConF (X,Y)) such that
A6: for h being set st h in [:(ConFuncs ((FlatPoset X),(FlatPoset Y))),(ConFuncs ((FlatPoset X),(FlatPoset Y))):] holds
W2 . h = RecFunc02 ((h `1),(h `2),E1,E2,I2,J2,D) by Threcursive0101;
reconsider W = <:W1,W2:> as continuous Function of [:(FlatConF (X,Y)),(FlatConF (X,Y)):],[:(FlatConF (X,Y)),(FlatConF (X,Y)):] by YELLOW_3:def 2;
reconsider h = least_fix_point W as Element of [:(FlatConF (X,Y)),(FlatConF (X,Y)):] ;
h is_a_fixpoint_of W by POSET_1:def 5;
then A7: h = W . h by ABIAN:def 3;
A8: ( W1 . h = RecFunc02 ((h `1),(h `2),E1,E2,I1,J1,D) & W2 . h = RecFunc02 ((h `1),(h `2),E1,E2,I2,J2,D) ) by A4, A5, A6;
consider f, g being Element of (FlatConF (X,Y)) such that
A9: h = [f,g] by ThProdPoset01;
take f ; :: thesis: ex g being set st
( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & g in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc02 (f,g,E1,E2,I1,J1,D) & g = RecFunc02 (f,g,E1,E2,I2,J2,D) )
take g ; :: thesis: ( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & g in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc02 (f,g,E1,E2,I1,J1,D) & g = RecFunc02 (f,g,E1,E2,I2,J2,D) )
dom W = the carrier of [:(FlatConF (X,Y)),(FlatConF (X,Y)):] by FUNCT_2:def 1;
then [f,g] = [(RecFunc02 (f,g,E1,E2,I1,J1,D)),(RecFunc02 (f,g,E1,E2,I2,J2,D))] by FUNCT_3:def 7, A7, A8, A9;
hence ( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & g in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc02 (f,g,E1,E2,I1,J1,D) & g = RecFunc02 (f,g,E1,E2,I2,J2,D) ) by XTUPLE_0:1; :: thesis: verum