let n be Nat; :: thesis: for P being non empty strict chain-complete Poset
for p being Element of P
for g being monotone Function of P,P holds (iter g,n) . p is Element of P
let P be non empty strict chain-complete Poset; :: thesis: for p being Element of P
for g being monotone Function of P,P holds (iter g,n) . p is Element of P
let p be Element of P; :: thesis: for g being monotone Function of P,P holds (iter g,n) . p is Element of P
let g be monotone Function of P,P; :: thesis: (iter g,n) . p is Element of P
set X = the carrier of P;
reconsider g1 = iter g,n as Function of the carrier of P,the carrier of P by Lemiter03;
g1 . p in the carrier of P ;
hence (iter g,n) . p is Element of P ; :: thesis: verum