let X, Y be non empty set ; :: thesis:
let D be Subset of X; :: thesis:
let I be Function of X,Y; :: thesis:
let J be Function of [:X,Y:],Y; :: thesis:
let E be Function of X,X; :: thesis:
set z = X;
set r = Y;
set FX = FlatPoset X;
set CX = succ X;
set FY = FlatPoset Y;
set CY = succ Y;
set FlatC = FlatConF (X,Y);
set CFXY = ConFuncs ((FlatPoset X),(FlatPoset Y));
set CRFXY = ConRelat ((FlatPoset X),(FlatPoset Y));
deffunc H₁( object ) -> continuous Function of (FlatPoset X),(FlatPoset Y) = RecFunc01 ($1,E,I,J,D);
A7: for h being continuous Function of (FlatPoset X),(FlatPoset Y) holds h in ConFuncs ((FlatPoset X),(FlatPoset Y))

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;

proof

B2: for f being continuous Function of (FlatPoset X),(FlatPoset Y) ex g being continuous Function of (FlatPoset X),(FlatPoset Y) st g = IT . f

proof

let f be continuous Function of (FlatPoset X),(FlatPoset Y); :: thesis:
set g = IT . f;
f in ConFuncs ((FlatPoset X),(FlatPoset Y)) by A7;
then reconsider g = IT . f as continuous Function of (FlatPoset X),(FlatPoset Y) by A8, FUNCT_2:5;
take g ; :: thesis:
thus g = IT . f ; :: thesis:

end;

B3: for f, g being continuous Function of (FlatPoset X),(FlatPoset Y) st g = IT . f holds
for x being Element of (FlatPoset X) holds g . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D)

proof

let f, g be continuous Function of (FlatPoset X),(FlatPoset Y); :: thesis:
assume C1: g = IT . f ; :: thesis:
for x being Element of (FlatPoset X) holds g . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D)

proof

let x be Element of (FlatPoset X); :: thesis:
g . x = (RecFunc01 (f,E,I,J,D)) . x by A7, A10, C1
.= BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) by DefRecFunc01 ;
hence g . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) ; :: thesis:

end;

hence for x being Element of (FlatPoset X) holds g . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) ; :: thesis:

end;

reconsider IT = IT as Function of (FlatConF (X,Y)),(FlatConF (X,Y)) ;
IT is monotone

proof

for f1, f2 being Element of (FlatConF (X,Y)) st f1 <= f2 holds
for g1, g2 being Element of (FlatConF (X,Y)) st g1 = IT . f1 & g2 = IT . f2 holds
g1 <= g2

proof

let f1, f2 be Element of (FlatConF (X,Y)); :: 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:
consider f10, f20 being Function of (FlatPoset X),(FlatPoset Y) such that
C401: ( f1 = f10 & f2 = f20 & f10 <= f20 ) by POSET_1:def 7, C1;
reconsider f10 = f10, f20 = f20 as continuous Function of (FlatPoset X),(FlatPoset Y) by C401, A8;
reconsider g10 = g1 as continuous Function of (FlatPoset X),(FlatPoset Y) by A8;
reconsider 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 y = (Flatten E) . x as Element of (FlatPoset X) ;
set y1 = f10 . y;
set y2 = f20 . y;
D1: g10 . x = BaseFunc01 (x,(f10 . y),I,J,D) by B3, C2, C401;
D2: g20 . x = BaseFunc01 (x,(f20 . y),I,J,D) by B3, C2, C401;

per cases by ThFlatten04, C401, YELLOW_2:9;

suppose f10 . y = Y ; :: thesis:

then D000: not f10 . y in Y ;

per cases ;

suppose D001: x in D ; :: thesis:

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

end;

suppose not x in D ; :: thesis:

then g10 . x = Y by D000, D1, DefBaseFunc01;
hence g10 . x <= g20 . x by LemFlatten02; :: thesis:

end;

suppose f10 . y = f20 . y ; :: thesis:

hence g10 . x <= g20 . x by D1, B3, C2, C401; :: thesis:

end;

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

end;

hence IT is monotone ; :: thesis:

end;

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

proof

let F be non empty Chain of (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, G = G as non empty Chain of (ConPoset ((FlatPoset X),(FlatPoset Y))) ;
set sf = sup F;
D1: sup F = sup_func F by POSET_1:11;
then reconsider sf = sup F as continuous Function of (FlatPoset X),(FlatPoset Y) ;
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) ;
consider g being continuous Function of (FlatPoset X),(FlatPoset Y) such that
D5: g = IT . sf 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 E) . x as Element of (FlatPoset X) ;
reconsider M = F -image x1 as non empty Chain of (FlatPoset Y) ;
consider a being Element of (FlatPoset Y) such that
D000: ( M = {a} or M = {(Bottom (FlatPoset Y)),a} ) by Thflat01;
D001: sup M = a by D000, YELLOW_0:39, Thflat0502;
D002: g . x = BaseFunc01 (x,(sf . x1),I,J,D) by B3, D5
.= BaseFunc01 (x,a,I,J,D) by D001, POSET_1:def 10, D1 ;
a in F -image x1 by TARSKI:def 1, TARSKI:def 2, D000;
then consider q1 being Element of (FlatPoset Y) such that
D003: ( q1 = a & ex f1 being continuous Function of (FlatPoset X),(FlatPoset Y) st
( f1 in F & q1 = f1 . x1 ) ) ;
consider f1 being continuous Function of (FlatPoset X),(FlatPoset Y) such that
D004: ( f1 in F & a = f1 . x1 ) by D003;
reconsider f01 = f1 as Element of (FlatConF (X,Y)) by A7;
reconsider g01 = IT . f01 as continuous Function of (FlatPoset X),(FlatPoset Y) by A8;
D005: g01 . x = g . x by B3, D004, D002;
reconsider N = G -image x as non empty Chain of (FlatPoset Y) ;
D006: sg . x = sup N by POSET_1:def 10, D3;
dom IT = ConFuncs ((FlatPoset X),(FlatPoset Y)) by FUNCT_2:def 1;
then [f01,g01] in IT by FUNCT_1:def 2;
then g01 in IT .: F by RELAT_1:def 13, D004;
then g01 . x in N ;
hence g . x <= sg . x by D005, Thsup01, D006; :: thesis:

end;

then g <= sg by YELLOW_2:9;
hence IT . (sup F) <= sup G by D5, 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)) by POSET_1:8; :: thesis:

end;

then reconsider IT = IT as continuous Function of (FlatConF (X,Y)),(FlatConF (X,Y)) ;
for f being Element of ConFuncs ((FlatPoset X),(FlatPoset Y)) holds IT . f = RecFunc01 (f,E,I,J,D) by A10;
hence ex W being continuous Function of (FlatConF (X,Y)),(FlatConF (X,Y)) st
for f being Element of ConFuncs ((FlatPoset X),(FlatPoset Y)) holds W . f = RecFunc01 (f,E,I,J,D) ; :: thesis: