let P be non empty strict chain-complete Poset; :: thesis: for G being non empty Chain of (ConPoset P,P)
for x being set
for n being Nat
for M being non empty Chain of P
for g1 being monotone Function of P,P st 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,n) . (Bottom P) ) } & x in g1 .: M holds
ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter g,n) . (Bottom P)) )
let G be non empty Chain of (ConPoset P,P); :: thesis: for x being set
for n being Nat
for M being non empty Chain of P
for g1 being monotone Function of P,P st 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,n) . (Bottom P) ) } & x in g1 .: M holds
ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter g,n) . (Bottom P)) )
let x be set ; :: thesis: for n being Nat
for M being non empty Chain of P
for g1 being monotone Function of P,P st 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,n) . (Bottom P) ) } & x in g1 .: M holds
ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter g,n) . (Bottom P)) )
let n be Nat; :: thesis: for M being non empty Chain of P
for g1 being monotone Function of P,P st 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,n) . (Bottom P) ) } & x in g1 .: M holds
ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter g,n) . (Bottom P)) )
let M be non empty Chain of P; :: thesis: for g1 being monotone Function of P,P st 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,n) . (Bottom P) ) } & x in g1 .: M holds
ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter g,n) . (Bottom P)) )
let g1 be monotone Function of P,P; :: thesis: ( 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,n) . (Bottom P) ) } & x in g1 .: M implies ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter g,n) . (Bottom P)) ) )
assume A1: ( 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,n) . (Bottom P) ) } & x in g1 .: M ) ; :: thesis: ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter g,n) . (Bottom P)) )
then ex y being set st
( y in dom g1 & y in M & x = g1 . y ) by FUNCT_1:def 12;
then consider y being Element of M such that
A2: ( y in M & x = g1 . y ) ;
consider p being Element of P such that
A3: ( y = 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,n) . (Bottom P) ) ) by A1, A2;
thus ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter g,n) . (Bottom P)) ) by A2, A3; :: thesis: verum