proof

let h be continuous Function of (FlatPoset X),(FlatPoset Y); :: thesis:
h in Funcs ( the carrier of (FlatPoset X), the carrier of (FlatPoset Y)) by FUNCT_2:8;
hence h in ConFuncs ((FlatPoset X),(FlatPoset Y)) ; :: thesis:

end;

A8: for h being set st h in ConFuncs ((FlatPoset X),(FlatPoset Y)) holds
h is continuous Function of (FlatPoset X),(FlatPoset Y)

proof

let h be set ; :: thesis:
assume h in ConFuncs ((FlatPoset X),(FlatPoset Y)) ; :: thesis:
then consider x being Element of Funcs ( the carrier of (FlatPoset X), the carrier of (FlatPoset Y)) such that
B1: ( h = x & ex g being continuous Function of (FlatPoset X),(FlatPoset Y) st g = x ) ;
thus h is continuous Function of (FlatPoset X),(FlatPoset Y) by B1; :: thesis:

end;

A801: for h being Element of [:(FlatConF (X,Y)),(FlatConF (X,Y)):] ex h1, h2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h = [h1,h2]

proof

let h be Element of [:(FlatConF (X,Y)),(FlatConF (X,Y)):]; :: thesis:
B1: h is Element of [:(ConFuncs ((FlatPoset X),(FlatPoset Y))),(ConFuncs ((FlatPoset X),(FlatPoset Y))):] by YELLOW_3:def 2;
reconsider h1 = h `1 , h2 = h `2 as continuous Function of (FlatPoset X),(FlatPoset Y) by A8;
take h1 ; :: thesis:
take h2 ; :: thesis:
consider xx, y being object such that
hh: ( xx in ConFuncs ((FlatPoset X),(FlatPoset Y)) & y in ConFuncs ((FlatPoset X),(FlatPoset Y)) & h = [xx,y] ) by ZFMISC_1:def 2, B1;
thus h = [h1,h2] by hh; :: thesis:

end;

proof

B1: for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) holds IT . [f1,f2] = H₁([f1,f2])

proof

let f1, f2 be continuous Function of (FlatPoset X),(FlatPoset Y); :: thesis:
set f = [f1,f2];
( f1 in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f2 in ConFuncs ((FlatPoset X),(FlatPoset Y)) ) by A7;
then [f1,f2] in [:(ConFuncs ((FlatPoset X),(FlatPoset Y))),(ConFuncs ((FlatPoset X),(FlatPoset Y))):] by ZFMISC_1:def 2;
hence IT . [f1,f2] = H₁([f1,f2]) by A10; :: thesis:

end;

B2: for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) ex g being continuous Function of (FlatPoset X),(FlatPoset Y) st g = IT . [f1,f2]

proof

let f1, f2 be continuous Function of (FlatPoset X),(FlatPoset Y); :: thesis:
set f = [f1,f2];
( f1 in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f2 in ConFuncs ((FlatPoset X),(FlatPoset Y)) ) by A7;
then C1: [f1,f2] in [:(ConFuncs ((FlatPoset X),(FlatPoset Y))),(ConFuncs ((FlatPoset X),(FlatPoset Y))):] by ZFMISC_1:def 2;
reconsider g = IT . [f1,f2] as continuous Function of (FlatPoset X),(FlatPoset Y) by A8, C1, FUNCT_2:5;
take g ; :: thesis:
thus g = IT . [f1,f2] ; :: thesis:

end;

B3: for f1, f2, g being continuous Function of (FlatPoset X),(FlatPoset Y) st g = IT . [f1,f2] holds
for x being Element of (FlatPoset X) holds
( g . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D) & ( x in D implies g . x = I . x ) )

proof

let f1, f2 be continuous Function of (FlatPoset X),(FlatPoset Y); :: thesis:
let g be continuous Function of (FlatPoset X),(FlatPoset Y); :: thesis:
assume C1: g = IT . [f1,f2] ; :: thesis:
let x be Element of (FlatPoset X); :: thesis:
( [f1,f2] `1 = f1 & [f1,f2] `2 = f2 ) ;
then g . x = (RecFunc02 (f1,f2,E1,E2,I,J,D)) . x by B1, C1
.= BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D) by DefRecFunc02 ;
hence ( g . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D) & ( x in D implies g . x = I . x ) ) by DefBaseFunc02; :: thesis:

end;

reconsider IT = IT as Function of [:(FlatConF (X,Y)),(FlatConF (X,Y)):],(FlatConF (X,Y)) by A6;
IT is monotone

proof

let f1, f2 be Element of [:(FlatConF (X,Y)),(FlatConF (X,Y)):]; :: according to ORDERS_3:def 5 :: thesis:
assume C1: f1 <= f2 ; :: thesis:
let g1, g2 be Element of (FlatConF (X,Y)); :: thesis:
assume C2: ( g1 = IT . f1 & g2 = IT . f2 ) ; :: thesis:
reconsider f101 = f1 `1 , f102 = f1 `2 , f201 = f2 `1 , f202 = f2 `2 as Element of (FlatConF (X,Y)) ;
[f101,f201] in ConRelat ((FlatPoset X),(FlatPoset Y)) by ORDERS_2:def 5, C1, YELLOW_3:12;
then consider f1011, f2011 being Function of (FlatPoset X),(FlatPoset Y) such that
C301: ( f101 = f1011 & f201 = f2011 & f1011 <= f2011 ) by POSET_1:def 7;
reconsider f1011 = f1011, f2011 = f2011 as continuous Function of (FlatPoset X),(FlatPoset Y) by C301, A8;
[f102,f202] in ConRelat ((FlatPoset X),(FlatPoset Y)) by ORDERS_2:def 5, C1, YELLOW_3:12;
then consider f1021, f2021 being Function of (FlatPoset X),(FlatPoset Y) such that
C401: ( f102 = f1021 & f202 = f2021 & f1021 <= f2021 ) by POSET_1:def 7;
reconsider f1021 = f1021, f2021 = f2021 as continuous Function of (FlatPoset X),(FlatPoset Y) by C401, A8;
reconsider g10 = g1, g20 = g2 as continuous Function of (FlatPoset X),(FlatPoset Y) by A8;
for x being Element of (FlatPoset X) holds g10 . x <= g20 . x

proof

let x be Element of (FlatPoset X); :: thesis:
reconsider y01 = (Flatten E1) . x, y02 = (Flatten E2) . x as Element of (FlatPoset X) ;
set y1 = f1011 . y01;
set y2 = f2011 . y01;
set y3 = f1021 . y02;
set y4 = f2021 . y02;
f1 in the carrier of [:(FlatConF (X,Y)),(FlatConF (X,Y)):] ;
then f1 in [: the carrier of (FlatConF (X,Y)), the carrier of (FlatConF (X,Y)):] by YELLOW_3:def 2;
then consider xx, y being object such that
hh: ( xx in the carrier of (FlatConF (X,Y)) & y in the carrier of (FlatConF (X,Y)) & f1 = [xx,y] ) by ZFMISC_1:def 2;
D1: g10 = IT . [f1011,f1021] by C2, C401, hh, C301;
D101: g10 . x = BaseFunc02 (x,(f1011 . y01),(f1021 . y02),I,J,D) by B3, C2, C401, hh, C301;
f2 in the carrier of [:(FlatConF (X,Y)),(FlatConF (X,Y)):] ;
then f2 in [: the carrier of (FlatConF (X,Y)), the carrier of (FlatConF (X,Y)):] by YELLOW_3:def 2;
then consider xx, y being object such that
hh: ( xx in the carrier of (FlatConF (X,Y)) & y in the carrier of (FlatConF (X,Y)) & f2 = [xx,y] ) by ZFMISC_1:def 2;
D2: g20 = IT . [f2011,f2021] by C2, C401, C301, hh;

per cases by ThFlatten04, C301, YELLOW_2:9;

suppose f1011 . y01 = Y ; :: thesis:

then D301: not f1011 . y01 in Y ;

per cases ;

suppose D302: x in D ; :: thesis:

then g10 . x = I . x by D1, B3;
hence g10 . x <= g20 . x by D2, B3, D302; :: thesis:

end;

suppose not x in D ; :: thesis:

then g10 . x = Y by D301, D101, DefBaseFunc02;
hence g10 . x <= g20 . x by LemFlatten02; :: thesis:

end;

suppose D304: f1011 . y01 = f2011 . y01 ; :: thesis:

per cases by C401, YELLOW_2:9, ThFlatten04;

suppose f1021 . y02 = Y ; :: thesis:

then D305: not f1021 . y02 in Y ;

per cases ;

suppose D306: x in D ; :: thesis:

then g10 . x = I . x by D1, B3;
hence g10 . x <= g20 . x by D2, B3, D306; :: thesis:

end;

suppose not x in D ; :: thesis:

then g10 . x = Y by D305, D101, DefBaseFunc02;
hence g10 . x <= g20 . x by LemFlatten02; :: thesis:

end;

suppose f1021 . y02 = f2021 . y02 ; :: thesis:

hence g10 . x <= g20 . x by D101, C2, C401, C301, hh, B3, D304; :: thesis:

end;

then g10 <= g20 by YELLOW_2:9;
hence g1 <= g2 by POSET_1:def 7; :: thesis:

end;

then reconsider IT = IT as monotone Function of [:(FlatConF (X,Y)),(FlatConF (X,Y)):],(FlatConF (X,Y)) ;
for F being non empty Chain of [:(FlatConF (X,Y)),(FlatConF (X,Y)):] holds IT . (sup F) <= sup (IT .: F)

proof

let F be non empty Chain of [:(FlatConF (X,Y)),(FlatConF (X,Y)):]; :: thesis:
reconsider G = IT .: F as non empty Chain of (FlatConF (X,Y)) by POSET_1:1;
IT . (sup F) <= sup G

proof

reconsider F = F as non empty Chain of [:(ConPoset ((FlatPoset X),(FlatPoset Y))),(ConPoset ((FlatPoset X),(FlatPoset Y))):] ;
reconsider G = G as non empty Chain of (ConPoset ((FlatPoset X),(FlatPoset Y))) ;
D101: sup (proj1 F) = sup_func (proj1 F) by POSET_1:11;
then reconsider sf1 = sup (proj1 F) as continuous Function of (FlatPoset X),(FlatPoset Y) ;
D102: sup (proj2 F) = sup_func (proj2 F) by POSET_1:11;
then reconsider sf2 = sup (proj2 F) as continuous Function of (FlatPoset X),(FlatPoset Y) ;
D103: sup F = [sf1,sf2] by YELLOW_3:46, LemProdPoset06;
set sg = sup G;
D3: sup G = sup_func G by POSET_1:11;
then reconsider sg = sup G as continuous Function of (FlatPoset X),(FlatPoset Y) ;
D4: for x being Element of (FlatPoset X) st x in D holds
sg . x = I . x

proof

let x be Element of (FlatPoset X); :: thesis:
assume D401: x in D ; :: thesis:
reconsider N = G -image x as non empty Chain of (FlatPoset Y) ;
set h = the Element of G;
reconsider h = the Element of G as continuous Function of (FlatPoset X),(FlatPoset Y) by A8;
reconsider hx = h . x as Element of (FlatPoset Y) ;
D402: hx in N ;
consider f being Element of [:(ConFuncs ((FlatPoset X),(FlatPoset Y))),(ConFuncs ((FlatPoset X),(FlatPoset Y))):] such that
D403: ( f in F & h = IT . f ) by FUNCT_2:65;
reconsider f = f as Element of [:(FlatConF (X,Y)),(FlatConF (X,Y)):] by D403;
consider f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) such that
D404: f = [f1,f2] by A801;
D405: hx = I . x by B3, D401, D403, D404;
then hx in Y by FUNCT_2:5, D401;
then hx <> Y ;
then sup N = hx by ThFlatten04, D402, Thsup01;
hence sg . x = I . x by D405, POSET_1:def 10, D3; :: thesis:

end;

consider g being continuous Function of (FlatPoset X),(FlatPoset Y) such that
D5: g = IT . [sf1,sf2] by B2;
for x being Element of (FlatPoset X) holds g . x <= sg . x

proof

let x be Element of (FlatPoset X); :: thesis:
reconsider x1 = (Flatten E1) . x, x2 = (Flatten E2) . x as Element of (FlatPoset X) ;
reconsider M1 = (proj1 F) -image x1, M2 = (proj2 F) -image x2 as non empty Chain of (FlatPoset Y) ;
consider a1 being Element of (FlatPoset Y) such that
E401: ( M1 = {a1} or M1 = {(Bottom (FlatPoset Y)),a1} ) by Thflat01;
E402: sup M1 = a1

proof

per cases by E401;

suppose M1 = {a1} ; :: thesis:

hence sup M1 = a1 by YELLOW_0:39; :: thesis:

end;

suppose M1 = {(Bottom (FlatPoset Y)),a1} ; :: thesis:

hence sup M1 = a1 by Thflat0502; :: thesis:

end;

consider a2 being Element of (FlatPoset Y) such that
E403: ( M2 = {a2} or M2 = {(Bottom (FlatPoset Y)),a2} ) by Thflat01;
E404: sup M2 = a2

proof

per cases by E403;

suppose M2 = {a2} ; :: thesis:

hence sup M2 = a2 by YELLOW_0:39; :: thesis:

end;

suppose M2 = {(Bottom (FlatPoset Y)),a2} ; :: thesis:

hence sup M2 = a2 by Thflat0502; :: thesis:

end;

E0: ( sf1 . x1 = a1 & sf2 . x2 = a2 ) by POSET_1:def 10, D101, D102, E402, E404;
E1: g . x = BaseFunc02 (x,a1,a2,I,J,D) by B3, D5, E0;
E500: ( a1 in (proj1 F) -image x1 & a2 in (proj2 F) -image x2 ) by TARSKI:def 1, TARSKI:def 2, E401, E403;
consider q1 being Element of (FlatPoset Y) such that
E501: ( q1 = a1 & ex f1 being continuous Function of (FlatPoset X),(FlatPoset Y) st
( f1 in proj1 F & q1 = f1 . x1 ) ) by E500;
consider q2 being Element of (FlatPoset Y) such that
E502: ( q2 = a2 & ex f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st
( f2 in proj2 F & q2 = f2 . x2 ) ) by E500;

per cases ;

suppose E503: not x in D ; :: thesis:

per cases ;

suppose E504: ( a1 <> Y & a2 <> Y ) ; :: thesis:

ex f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st
( [f1,f2] in F & a1 = f1 . x1 & a2 = f2 . x2 )

proof

consider f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) such that
E600: ( f1 in proj1 F & a1 = f1 . x1 & f2 in proj2 F & a2 = f2 . x2 ) by E501, E502;
consider f12 being object such that
E601: [f1,f12] in F by E600, XTUPLE_0:def 12;
[f1,f12] `2 in ConFuncs ((FlatPoset X),(FlatPoset Y)) by MCART_1:10, A6, E601;
then reconsider f12 = f12 as continuous Function of (FlatPoset X),(FlatPoset Y) by A8;
consider f21 being object such that
E602: [f21,f2] in F by E600, XTUPLE_0:def 13;
[f21,f2] `1 in ConFuncs ((FlatPoset X),(FlatPoset Y)) by MCART_1:10, A6, E602;
then reconsider f21 = f21 as continuous Function of (FlatPoset X),(FlatPoset Y) by A8;
reconsider f1F = f1, f12F = f12, f2F = f2, f21F = f21 as Element of (FlatConF (X,Y)) by A7;
reconsider h1 = [f1F,f12F], h2 = [f21F,f2F] as Element of F by E601, E602;
reconsider h1 = h1, h2 = h2 as Element of [:(FlatConF (X,Y)),(FlatConF (X,Y)):] ;

per cases by ORDERS_2:11;

suppose h1 <= h2 ; :: thesis:

then f1F <= f21F by YELLOW_3:11;
then consider f, g being Function of (FlatPoset X),(FlatPoset Y) such that
G001: ( f1 = f & f21 = g & f <= g ) by POSET_1:def 7;
take f21 ; :: thesis:
take f2 ; :: thesis:
thus ( [f21,f2] in F & a1 = f21 . x1 & a2 = f2 . x2 ) by E602, E600, E504, ThFlatten04, YELLOW_2:9, G001; :: thesis:

end;

suppose h2 <= h1 ; :: thesis:

then f2F <= f12F by YELLOW_3:11;
then consider f, g being Function of (FlatPoset X),(FlatPoset Y) such that
G001: ( f2 = f & f12 = g & f <= g ) by POSET_1:def 7;
take f1 ; :: thesis:
take f12 ; :: thesis:
thus ( [f1,f12] in F & a1 = f1 . x1 & a2 = f12 . x2 ) by E601, E600, E504, ThFlatten04, YELLOW_2:9, G001; :: thesis:

end;

then consider f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) such that
E6: ( [f1,f2] in F & a1 = f1 . x1 & a2 = f2 . x2 ) ;
( f1 in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f2 in ConFuncs ((FlatPoset X),(FlatPoset Y)) ) by A7;
then reconsider f01 = [f1,f2] as Element of [:(FlatConF (X,Y)),(FlatConF (X,Y)):] by ZFMISC_1:def 2, A6;
reconsider g01 = IT . f01 as continuous Function of (FlatPoset X),(FlatPoset Y) by A8;
E7: g01 . x = g . x by B3, E6, E1;
reconsider N = G -image x as non empty Chain of (FlatPoset Y) ;
E9: sg . x = sup N by POSET_1:def 10, D3;
dom IT = [:(ConFuncs ((FlatPoset X),(FlatPoset Y))),(ConFuncs ((FlatPoset X),(FlatPoset Y))):] by FUNCT_2:def 1;
then [f01,g01] in IT by FUNCT_1:def 2, A6;
then g01 in IT .: F by RELAT_1:def 13, E6;
then g01 . x in N ;
hence g . x <= sg . x by E7, Thsup01, E9; :: thesis:

end;

suppose ( a1 = Y or a2 = Y ) ; :: thesis:

then ( not a1 in Y or not a2 in Y ) ;
then g . x = Y by E1, DefBaseFunc02, E503;
hence g . x <= sg . x by LemFlatten02; :: thesis:

end;

suppose E506: x in D ; :: thesis:

then sg . x = I . x by D4
.= g . x by E506, B3, D5 ;
hence g . x <= sg . x ; :: thesis:

end;

then g <= sg by YELLOW_2:9;
hence IT . (sup F) <= sup G by D5, D103, POSET_1:def 7; :: thesis:

end;

hence IT . (sup F) <= sup (IT .: F) ; :: thesis:

end;

hence IT is continuous Function of [:(FlatConF (X,Y)),(FlatConF (X,Y)):],(FlatConF (X,Y)) by POSET_1:8; :: thesis:

end;

then reconsider IT = IT as continuous Function of [:(FlatConF (X,Y)),(FlatConF (X,Y)):],(FlatConF (X,Y)) ;
for f being set st f in [:(ConFuncs ((FlatPoset X),(FlatPoset Y))),(ConFuncs ((FlatPoset X),(FlatPoset Y))):] holds
IT . f = RecFunc02 ((f `1),(f `2),E1,E2,I,J,D) by A10;
hence ex W being continuous Function of [:(FlatConF (X,Y)),(FlatConF (X,Y)):],(FlatConF (X,Y)) st
for f being set st f in [:(ConFuncs ((FlatPoset X),(FlatPoset Y))),(ConFuncs ((FlatPoset X),(FlatPoset Y))):] holds
W . f = RecFunc02 ((f `1),(f `2),E1,E2,I,J,D) ; :: thesis: