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 st p is_a_fixpoint_of g holds
(iter (g,n)) . p = 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 st p is_a_fixpoint_of g holds
(iter (g,n)) . p = p
let p be Element of P; :: thesis: for g being monotone Function of P,P st p is_a_fixpoint_of g holds
(iter (g,n)) . p = p
let g be monotone Function of P,P; :: thesis: ( p is_a_fixpoint_of g implies (iter (g,n)) . p = p )
defpred S1[ Nat] means for p being Element of P st p is_a_fixpoint_of g holds
(iter (g,$1)) . p = p;
A1: S1[ 0 ] by Lm1;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[k + 1]
S1[k + 1]
proof
let p be Element of P; :: thesis: ( p is_a_fixpoint_of g implies (iter (g,(k + 1))) . p = p )
assume A4: p is_a_fixpoint_of g ; :: thesis: (iter (g,(k + 1))) . p = p
iter (g,(k + 1)) = g * (iter (g,k)) by FUNCT_7:71;
then (iter (g,(k + 1))) . p = g . ((iter (g,k)) . p) by Lm2
.= g . p by A4, A3
.= p by A4, ABIAN:def 3 ;
hence (iter (g,(k + 1))) . p = p ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A1, A2);
 hence ( p is_a_fixpoint_of g implies (iter (g,n)) . p = p ) ; :: thesis: verum