let n be Nat; 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 p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,n)) . p3 holds
p1 <= p4
let P be non empty strict chain-complete Poset; for p, p1, p3, p4 being Element of P
for g being monotone Function of P,P st p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,n)) . p3 holds
p1 <= p4
let p, p1, p3, p4 be Element of P; for g being monotone Function of P,P st p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,n)) . p3 holds
p1 <= p4
let g be monotone Function of P,P; ( p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,n)) . p3 implies p1 <= p4 )
defpred S1[ Nat] means for p, p3, p1, p4 being Element of P st p <= p3 & p1 = (iter (g,$1)) . p & p4 = (iter (g,$1)) . p3 holds
p1 <= p4;
A1:
S1[ 0 ]
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A3:
for
p,
p3,
p1,
p4 being
Element of
P st
p <= p3 &
p1 = (iter (g,k)) . p &
p4 = (iter (g,k)) . p3 holds
p1 <= p4
;
S1[k + 1]
S1[
k + 1]
proof
let p,
p3,
p1,
p4 be
Element of
P;
( p <= p3 & p1 = (iter (g,(k + 1))) . p & p4 = (iter (g,(k + 1))) . p3 implies p1 <= p4 )
assume A4:
(
p <= p3 &
p1 = (iter (g,(k + 1))) . p &
p4 = (iter (g,(k + 1))) . p3 )
;
p1 <= p4
reconsider x1 =
(iter (g,k)) . p as
Element of
P ;
reconsider y1 =
(iter (g,k)) . p3 as
Element of
P ;
A5:
x1 <= y1
by A4, A3;
iter (
g,
(k + 1))
= g * (iter (g,k))
by FUNCT_7:71;
then
(
p1 = g . ((iter (g,k)) . p) &
p4 = g . ((iter (g,k)) . p3) )
by Lm2, A4;
hence
p1 <= p4
by A5, ORDERS_3:def 5;
verum
end;
hence
S1[
k + 1]
;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A2);
hence
( p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,n)) . p3 implies p1 <= p4 )
; verum