let n be Nat; for P being non empty strict chain-complete Poset
for p, p1, p2 being Element of P
for g1, g2 being monotone Function of P,P st g1 <= g2 & p1 = (iter (g1,n)) . p & p2 = (iter (g2,n)) . p holds
p1 <= p2
let P be non empty strict chain-complete Poset; for p, p1, p2 being Element of P
for g1, g2 being monotone Function of P,P st g1 <= g2 & p1 = (iter (g1,n)) . p & p2 = (iter (g2,n)) . p holds
p1 <= p2
let p, p1, p2 be Element of P; for g1, g2 being monotone Function of P,P st g1 <= g2 & p1 = (iter (g1,n)) . p & p2 = (iter (g2,n)) . p holds
p1 <= p2
let g1, g2 be monotone Function of P,P; ( g1 <= g2 & p1 = (iter (g1,n)) . p & p2 = (iter (g2,n)) . p implies p1 <= p2 )
defpred S1[ Nat] means for p, p1, p2 being Element of P st g1 <= g2 & p1 = (iter (g1,$1)) . p & p2 = (iter (g2,$1)) . p holds
p1 <= p2;
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:
S1[
k]
;
S1[k + 1]
S1[
k + 1]
proof
let p,
p1,
p2 be
Element of
P;
( g1 <= g2 & p1 = (iter (g1,(k + 1))) . p & p2 = (iter (g2,(k + 1))) . p implies p1 <= p2 )
assume A4:
(
g1 <= g2 &
p1 = (iter (g1,(k + 1))) . p &
p2 = (iter (g2,(k + 1))) . p )
;
p1 <= p2
reconsider q1 =
(iter (g1,k)) . p as
Element of
P ;
reconsider q2 =
(iter (g2,k)) . p as
Element of
P ;
set r =
g1 . q2;
A5:
q1 <= q2
by A4, A3;
iter (
g1,
(k + 1))
= g1 * (iter (g1,k))
by FUNCT_7:71;
then A6:
p1 = g1 . q1
by Lm2, A4;
iter (
g2,
(k + 1))
= g2 * (iter (g2,k))
by FUNCT_7:71;
then A7:
p2 = g2 . q2
by Lm2, A4;
A8:
p1 <= g1 . q2
by A5, A6, ORDERS_3:def 5;
g1 . q2 <= p2
by A4, A7, YELLOW_2:9;
hence
p1 <= p2
by A8, ORDERS_2:3;
verum
end;
hence
S1[
k + 1]
;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A2);
hence
( g1 <= g2 & p1 = (iter (g1,n)) . p & p2 = (iter (g2,n)) . p implies p1 <= p2 )
; verum