let n be Nat; :: thesis: for P being non empty strict chain-complete Poset
for p1, p, 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; :: thesis: for p1, p, 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 p1, p, p2 be Element of P; :: thesis: 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; :: thesis: ( g1 <= g2 & p1 = (iter g1,n) . p & p2 = (iter g2,n) . p implies p1 <= p2 )
defpred S₁[ 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: S₁[ 0 ]

proof

let p, p1, p2 be Element of P; :: thesis: ( g1 <= g2 & p1 = (iter g1,0 ) . p & p2 = (iter g2,0 ) . p implies p1 <= p2 )
assume ( g1 <= g2 & p1 = (iter g1,0 ) . p & p2 = (iter g2,0 ) . p ) ; :: thesis: p1 <= p2
then ( p1 = p & p2 = p ) by Lemiter10;
hence p1 <= p2 ; :: thesis: verum

end;

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, p1, p2 be Element of P; :: thesis: ( g1 <= g2 & p1 = (iter g1,(k + 1)) . p & p2 = (iter g2,(k + 1)) . p implies p1 <= p2 )
assume B1: ( g1 <= g2 & p1 = (iter g1,(k + 1)) . p & p2 = (iter g2,(k + 1)) . p ) ; :: thesis: p1 <= p2
reconsider q1 = (iter g1,k) . p as Element of P by Lemiter11;
reconsider q2 = (iter g2,k) . p as Element of P by Lemiter11;
set r = g1 . q2;
B2: q1 <= q2 by B1, A3;
B03: iter g1,(k + 1) = g1 * (iter g1,k) by FUNCT_7:73;
B3: p1 = g1 . q1 by B03, Lemiter12, B1;
B04: iter g2,(k + 1) = g2 * (iter g2,k) by FUNCT_7:73;
B4: p2 = g2 . q2 by B04, Lemiter12, B1;
B5: p1 <= g1 . q2 by B2, B3, ORDERS_3:def 5;
g1 . q2 <= p2 by YELLOW_2:10, B1, B4;
hence p1 <= p2 by B5, ORDERS_2:26; :: 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 ( g1 <= g2 & p1 = (iter g1,n) . p & p2 = (iter g2,n) . p implies p1 <= p2 ) ; :: thesis: verum