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 Lm5;
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 A4: ( 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 Lm6;
reconsider q2 = (iter (g2,k)) . p as Element of P by Lm6;
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 Lm7, A4;
iter (g2,(k + 1)) = g2 * (iter (g2,k)) by FUNCT_7:71;
then A7: p2 = g2 . q2 by Lm7, 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; :: 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