let P be non empty strict chain-complete Poset; :: thesis: for g being monotone Function of P,P holds sup (iter_min g) = sup (g .: (iter_min g))
let g be monotone Function of P,P; :: thesis: sup (iter_min g) = sup (g .: (iter_min g))
reconsider L = g .: (iter_min g) as non empty Chain of P by Th1;
A1: ( ex_sup_of iter_min g,P & ex_sup_of L,P ) by Def1;
set a = Bottom P;
set s1 = sup (iter_min g);
set s2 = sup L;
A2: iter_min g is_<=_than sup (iter_min g) by A1, YELLOW_0:def 9;
A3: L is_<=_than sup L by A1, YELLOW_0:def 9;
for x being Element of P st x in iter_min g holds
x <= sup L
proof
let x be Element of P; :: thesis: ( x in iter_min g implies x <= sup L )
assume x in iter_min g ; :: thesis: x <= sup L
then consider p being Element of P such that
A4: ( x = p & ex n being Nat st p = (iter (g,n)) . (Bottom P) ) ;
consider n being Nat such that
A5: p = (iter (g,n)) . (Bottom P) by A4;
A6: ( 1 <= n implies p in L )
proof
assume 1 <= n ; :: thesis: p in L
then consider k being Nat such that
A7: n = 1 + k by NAT_1:10;
reconsider z = (iter (g,k)) . (Bottom P) as Element of P ;
z in the carrier of P ;
then A8: ( z in dom g & z in iter_min g ) by FUNCT_2:def 1;
p = (g * (iter (g,k))) . (Bottom P) by A5, A7, FUNCT_7:71
.= g . z by Lm2 ;
hence p in L by A8, FUNCT_1:def 6; :: thesis: verum
end;
( n = 0 implies p = Bottom P ) by A5, Lm1;
hence x <= sup L by A6, A4, A3, NAT_1:14, YELLOW_0:44; :: thesis: verum
end;
then iter_min g is_<=_than sup L ;
then A9: sup (iter_min g) <= sup L by A1, YELLOW_0:30;
for x being Element of P st x in L holds
x <= sup (iter_min g)
proof
let x be Element of P; :: thesis: ( x in L implies x <= sup (iter_min g) )
assume x in L ; :: thesis: x <= sup (iter_min g)
then consider z being object such that
A10: ( z in dom g & z in iter_min g & x = g . z ) by FUNCT_1:def 6;
consider z1 being Element of P such that
A11: ( z = z1 & ex n being Nat st z1 = (iter (g,n)) . (Bottom P) ) by A10;
consider n being Nat such that
A12: z1 = (iter (g,n)) . (Bottom P) by A11;
set n1 = n + 1;
g . z = (g * (iter (g,n))) . (Bottom P) by Lm2, A11, A12
.= (iter (g,(n + 1))) . (Bottom P) by FUNCT_7:71 ;
then x in iterSet (g,(Bottom P)) by A10;
hence x <= sup (iter_min g) by A2; :: thesis: verum
end;
then L is_<=_than sup (iter_min g) ;
then sup L <= sup (iter_min g) by A1, YELLOW_0:def 9;
hence sup (iter_min g) = sup (g .: (iter_min g)) by A9, ORDERS_2:2; :: thesis: verum