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
( (g * (iter (g,n))) . p = g . ((iter (g,n)) . p) & ((iter (g,n)) * g) . p = (iter (g,n)) . (g . 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
( (g * (iter (g,n))) . p = g . ((iter (g,n)) . p) & ((iter (g,n)) * g) . p = (iter (g,n)) . (g . p) )
let p be Element of P; :: thesis: for g being monotone Function of P,P holds
( (g * (iter (g,n))) . p = g . ((iter (g,n)) . p) & ((iter (g,n)) * g) . p = (iter (g,n)) . (g . p) )
let g be monotone Function of P,P; :: thesis: ( (g * (iter (g,n))) . p = g . ((iter (g,n)) . p) & ((iter (g,n)) * g) . p = (iter (g,n)) . (g . 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;
( (g * g1) . p = g . (g1 . p) & (g1 * g) . p = g1 . (g . p) ) by FUNCT_2:15;
hence ( (g * (iter (g,n))) . p = g . ((iter (g,n)) . p) & ((iter (g,n)) * g) . p = (iter (g,n)) . (g . p) ) ; :: thesis: verum