let P be non empty Poset; :: thesis: for g being monotone Function of P,P
for p being Element of P holds (iter (g,0)) . p = p
let g be monotone Function of P,P; :: thesis: for p being Element of P holds (iter (g,0)) . p = p
let p be Element of P; :: thesis: (iter (g,0)) . p = p
set X = the carrier of P;
(iter (g,0)) . p = (id the carrier of P) . p by FUNCT_7:84
.= p ;
hence (iter (g,0)) . p = p ; :: thesis: verum