let n, k be Nat; for P being non empty strict chain-complete Poset
for p3, p, p1, 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; for p3, p, p1, 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 p3, p, p1, p4 be 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 g be monotone Function of P,P; ( p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p implies p1 <= p4 )
defpred S1[ 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:
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
p3 = g . p &
p <= p3 &
p1 = (iter (g,n)) . p &
p4 = (iter (g,(n + k))) . p holds
p1 <= p4
;
S1[k + 1]
S1[
k + 1]
proof
let p,
p3,
p1,
p4 be
Element of
P;
( p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + (k + 1)))) . p implies p1 <= p4 )
assume B1:
(
p3 = g . p &
p <= p3 &
p1 = (iter (g,n)) . p &
p4 = (iter (g,(n + (k + 1)))) . p )
;
p1 <= p4
reconsider y1 =
(iter (g,(n + k))) . p as
Element of
P by Lemiter11;
B2:
p1 <= y1
by B1, A3;
iter (
g,
(n + (k + 1))) =
iter (
g,
((n + k) + 1))
.=
(iter (g,(n + k))) * g
by FUNCT_7:71
;
then
p4 = (iter (g,(n + k))) . p3
by Lemiter12, B1;
then
y1 <= p4
by B1, Lemiter13;
hence
p1 <= p4
by B2, ORDERS_2:26;
verum
end;
hence
S1[
k + 1]
;
verum
end;
for k being Nat holds S1[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 )
; verum