let n, k be Nat; :: thesis: for P being non empty strict chain-complete Poset
for p, p1, p3, p4 being Element of P
for g being monotone Function of P,P st p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p holds
p1 <= p4
let P be non empty strict chain-complete Poset; :: thesis: for p, p1, p3, p4 being Element of P
for g being monotone Function of P,P st p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p holds
p1 <= p4
let p, p1, p3, p4 be Element of P; :: thesis: for g being monotone Function of P,P st p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p holds
p1 <= p4
let g be monotone Function of P,P; :: thesis: ( p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p implies p1 <= p4 )
defpred S₁[ Nat] means for p, p3, p1, p4 being Element of P st p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + $1))) . p holds
p1 <= p4;
A1: S₁[ 0 ] ;
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: for p, p3, p1, p4 being Element of P st p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p holds
p1 <= p4 ; :: thesis: S₁[k + 1]
S₁[k + 1]

proof

let p, p3, p1, p4 be Element of P; :: thesis: ( p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + (k + 1)))) . p implies p1 <= p4 )
assume A4: ( p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + (k + 1)))) . p ) ; :: thesis: p1 <= p4
reconsider y1 = (iter (g,(n + k))) . p as Element of P ;
A5: p1 <= y1 by A4, A3;
iter (g,(n + (k + 1))) = iter (g,((n + k) + 1))
.= (iter (g,(n + k))) * g by FUNCT_7:69 ;
then p4 = (iter (g,(n + k))) . p3 by Lm2, A4;
then y1 <= p4 by A4, Lm3;
hence p1 <= p4 by A5, ORDERS_2:3; :: 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 ( p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p implies p1 <= p4 ) ; :: thesis: verum