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 S₁[ Nat] means for p being Element of P st p is_a_fixpoint_of g holds
(iter (g,$1)) . p = p;
A1: S₁[ 0 ] by Lm1;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
S₁[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 S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence ( p is_a_fixpoint_of g implies (iter (g,n)) . p = p ) ; :: thesis: verum