let P be non empty strict chain-complete Poset; :: thesis: for G being non empty Chain of (ConPoset P,P) holds (fix_func P) . (sup G) <= sup ((fix_func P) .: G)
let G be non empty Chain of (ConPoset P,P); :: thesis: (fix_func P) . (sup G) <= sup ((fix_func P) .: G)
reconsider h = fix_func P as monotone Function of (ConPoset P,P),P by LemFix0201;
h . (sup G) <= sup (h .: G)

proof

reconsider L = h .: G as non empty Chain of P by ThChain1;
set g0 = sup G;
set p0 = h . (sup G);
reconsider G0 = sup G as continuous Function of P,P by LemCastFunc01;
B2: h . (sup G) = least_fix_point G0 by Deffixfunc;
B3: sup G = sup_func G by ThConPoset01;
then reconsider g0 = sup G as continuous Function of P,P ;
set a = Bottom P;
reconsider I0 = iterSet g0,(Bottom P) as non empty Chain of P by ThiterSet1;
B4: h . (sup G) = sup (iter_min g0) by Thfixpoint01, B2
.= sup I0 ;
B5: ex_sup_of I0,P by DefchainComplete;
for x being Element of P st x in I0 holds
x <= sup L

proof

let x be Element of P; :: thesis: ( x in I0 implies x <= sup L )
assume x in I0 ; :: thesis: x <= sup L
then consider y being Element of P such that
C1: ( x = y & ex n being Nat st y = (iter g0,n) . (Bottom P) ) ;
consider n0 being Nat such that
C2: x = (iter g0,n0) . (Bottom P) by C1;
set M0 = { p where p is Element of P : ex g being Element of (ConPoset P,P) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter h,n0) . (Bottom P) ) } ;
reconsider M0 = { p where p is Element of P : ex g being Element of (ConPoset P,P) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter h,n0) . (Bottom P) ) } as non empty Chain of P by LemFix04;
for p being Element of P st p in M0 holds
p <= sup L

proof

let p be Element of P; :: thesis: ( p in M0 implies p <= sup L )
assume p in M0 ; :: thesis: p <= sup L
then consider p0 being Element of P, g being continuous Function of P,P such that
D1: ( p = p0 & g in G & p0 = (iter g,n0) . (Bottom P) ) by LemFix02;
set r = h . g;
h . g in L by D1, LemFix0503;
then reconsider r = h . g as Element of P ;
D4: r <= sup L by Lem201, D1, LemFix0503;
p <= r by D1, LemFix0504;
hence p <= sup L by D4, ORDERS_2:26; :: thesis: verum

end;

then C3: sup M0 <= sup L by Lem202;
defpred S₁[ Nat] means for z being Element of P
for M being non empty Chain of P st z = (iter g0,$1) . (Bottom P) & M = { p where p is Element of P : ex g being Element of (ConPoset P,P) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter h,$1) . (Bottom P) ) } holds
z <= sup M;
C4: S₁[ 0 ]

proof

let z be Element of P; :: thesis: for M being non empty Chain of P st z = (iter g0,0 ) . (Bottom P) & M = { p where p is Element of P : ex g being Element of (ConPoset P,P) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter h,0 ) . (Bottom P) ) } holds
z <= sup M
let M be non empty Chain of P; :: thesis: ( z = (iter g0,0 ) . (Bottom P) & M = { p where p is Element of P : ex g being Element of (ConPoset P,P) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter h,0 ) . (Bottom P) ) } implies z <= sup M )
assume z = (iter g0,0 ) . (Bottom P) ; :: thesis: ( not M = { p where p is Element of P : ex g being Element of (ConPoset P,P) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter h,0 ) . (Bottom P) ) } or z <= sup M )
then z = Bottom P by Lemiter10;
hence ( not M = { p where p is Element of P : ex g being Element of (ConPoset P,P) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter h,0 ) . (Bottom P) ) } or z <= sup M ) by YELLOW_0:44; :: thesis: verum

end;

C5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume D1: S₁[k] ; :: thesis: S₁[k + 1]
for z1 being Element of P
for M1 being non empty Chain of P st z1 = (iter g0,(k + 1)) . (Bottom P) & M1 = { p where p is Element of P : ex g being Element of (ConPoset P,P) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter h,(k + 1)) . (Bottom P) ) } holds
z1 <= sup M1

proof

let z1 be Element of P; :: thesis: for M1 being non empty Chain of P st z1 = (iter g0,(k + 1)) . (Bottom P) & M1 = { p where p is Element of P : ex g being Element of (ConPoset P,P) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter h,(k + 1)) . (Bottom P) ) } holds
z1 <= sup M1
let M1 be non empty Chain of P; :: thesis: ( z1 = (iter g0,(k + 1)) . (Bottom P) & M1 = { p where p is Element of P : ex g being Element of (ConPoset P,P) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter h,(k + 1)) . (Bottom P) ) } implies z1 <= sup M1 )
assume E1: ( z1 = (iter g0,(k + 1)) . (Bottom P) & M1 = { p where p is Element of P : ex g being Element of (ConPoset P,P) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter h,(k + 1)) . (Bottom P) ) } ) ; :: thesis: z1 <= sup M1
reconsider z = (iter g0,k) . (Bottom P) as Element of P by Lemiter11;
E2: z1 = (g0 * (iter g0,k)) . (Bottom P) by E1, FUNCT_7:73
.= g0 . z by Lemiter12 ;
reconsider M = { p where p is Element of P : ex g being Element of (ConPoset P,P) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter h,k) . (Bottom P) ) } as non empty Chain of P by LemFix04;
reconsider M0 = g0 .: M as non empty Chain of P by ThChain1;
E3: g0 . (sup M) = sup M0 by Thcontinuous01;
E401: ex_sup_of M0,P by DefchainComplete;
for q being Element of P st q in M0 holds
q <= sup M1

proof

let q be Element of P; :: thesis: ( q in M0 implies q <= sup M1 )
assume q in M0 ; :: thesis: q <= sup M1
then consider g being continuous Function of P,P such that
F1: ( g in G & q = g0 . ((iter g,k) . (Bottom P)) ) by LemFix0505;
reconsider a1 = (iter g,k) . (Bottom P) as Element of P by Lemiter11;
reconsider W = G -image a1 as non empty Chain of P ;
F2: q = sup W by F1, Defsupfunc, B3;
F3: ex_sup_of W,P by DefchainComplete;
for q1 being Element of P st q1 in W holds
q1 <= sup M1

proof

let q1 be Element of P; :: thesis: ( q1 in W implies q1 <= sup M1 )
assume q1 in W ; :: thesis: q1 <= sup M1
then consider q2 being Element of P such that
F401: ( q1 = q2 & ex g1 being continuous Function of P,P st
( g1 in G & q2 = g1 . a1 ) ) ;
consider g1 being continuous Function of P,P such that
F402: ( g1 in G & q1 = g1 . a1 ) by F401;

per cases ( g1 <= g or g <= g1 ) by F1, F402, LemFix0401;

suppose g1 <= g ; :: thesis: q1 <= sup M1

then F404: q1 <= g . a1 by YELLOW_2:10, F402;
set a2 = g . a1;
reconsider g2 = g as Element of (ConPoset P,P) by LemCastFunc02;
reconsider gg = g2 as continuous Function of P,P ;
g . a1 = (g * (iter g,k)) . (Bottom P) by Lemiter12
.= (iter gg,(k + 1)) . (Bottom P) by FUNCT_7:73 ;
then g . a1 in M1 by E1, F1;
then g . a1 <= sup M1 by Lem201;
hence q1 <= sup M1 by F404, ORDERS_2:26; :: thesis: verum

end;

suppose F405: g <= g1 ; :: thesis: q1 <= sup M1

reconsider a2 = (iter g1,k) . (Bottom P) as Element of P by Lemiter11;
a1 <= a2 by F405, Lemiter17;
then F406: q1 <= g1 . a2 by ORDERS_3:def 5, F402;
set a3 = g1 . a2;
reconsider g2 = g1 as Element of (ConPoset P,P) by LemCastFunc02;
reconsider gg = g2 as continuous Function of P,P ;
g1 . a2 = (g1 * (iter g1,k)) . (Bottom P) by Lemiter12
.= (iter gg,(k + 1)) . (Bottom P) by FUNCT_7:73 ;
then g1 . a2 in M1 by E1, F402;
then g1 . a2 <= sup M1 by Lem201;
hence q1 <= sup M1 by F406, ORDERS_2:26; :: thesis: verum

end;

end;

end;

then W is_<=_than sup M1 by LATTICE3:def 9;
hence q <= sup M1 by F2, F3, YELLOW_0:def 9; :: thesis: verum

end;

then M0 is_<=_than sup M1 by LATTICE3:def 9;
then E4: sup M0 <= sup M1 by E401, YELLOW_0:def 9;
z <= sup M by D1;
then z1 <= sup M0 by E2, E3, ORDERS_3:def 5;
hence z1 <= sup M1 by E4, ORDERS_2:26; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(C4, C5);
then x <= sup M0 by C2;
hence x <= sup L by C3, ORDERS_2:26; :: thesis: verum

end;

then I0 is_<=_than sup L by LATTICE3:def 9;
hence h . (sup G) <= sup (h .: G) by B4, B5, YELLOW_0:def 9; :: thesis: verum

end;

hence (fix_func P) . (sup G) <= sup ((fix_func P) .: G) ; :: thesis: verum