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 Lm3;
g1 . p in the carrier of P ;
hence (iter (g,n)) . p is Element of P ; :: thesis: verum