let X, Y be non empty set ; 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; 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; 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; 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; 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
; 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
; ( 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; verum