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:86
.= p by FUNCT_1:35 ;
hence (iter g,0 ) . p = p ; :: thesis: verum